(*Compilar con Coq ver. 6.3.1*)
AddPath "/home/maxi/Doctorado/TesisMaestria".
AddPath "/home/maxi/Lifia/Lisex/LSM0.0".
AddPath "d:\\maximiliano\\Doctorado\\TesisMaestria".
Compile Module ListFunctions.
Compile Module ListSet.
Compile Module SFSstate.
Compile Module DACandMAC.
Compile Module setACLdata.

Compile Module chmod.
Compile Module addUsrGrpToAcl.
Compile Module chobjsc.
Compile Module chown.
Compile Module delUsrGrpFromAcl.
Compile Module aclstat.
Compile Module chsubsc.
Compile Module close.
Compile Module create.
Compile Module mkdir.
Compile Module open.
Compile Module oscstat.
Compile Module owner_close.
Compile Module read.
Compile Module readdir.
Compile Module rmdir.
Compile Module sscstat.
Compile Module stat.
Compile Module unlink.
Compile Module write.

Compile Module TransFunc.
Compile Module ModelProperties.
Compile Module AuxiliaryLemmas.

Compile Module aclstatIsSecure.
Compile Module oscstatIsSecure.
Compile Module readIsSecure.
Compile Module readdirIsSecure.
Compile Module statIsSecure.

Compile Module sscstatIsSecure.
Compile Module writeIsSecure.

Compile Module addUsrGrpToAclIsSecure.
Compile Module chmodIsSecure.
Compile Module chownIsSecure.
Compile Module delUsrGrpFromAclIsSecure.

Compile Module chobjscIsSecure.
Compile Module chsubscIsSecure.

Compile Module createIsSecure.
Compile Module mkdirIsSecure.
Compile Module unlinkIsSecure.
Compile Module rmdirIsSecure.

Compile Module closeIsSecure.
Compile Module owner_closeIsSecure.

Compile Module openIsSecure.

Compile Module InitialState.
Compile Module ModelLemmas.
