# # ChangeLog for src/LTL/LTLToLIN.ma # # Generated by Trac 1.2 # Feb 28, 2021, 2:44:34 PM Fri, 18 Nov 2011 12:03:14 GMT campbell [1515] * src/ASM/ASM.ma (modified) * src/ASM/Erase.ma (modified) * src/ASM/I8051.ma (modified) * src/ASM/Interpret.ma (modified) * src/ASM/Interpret2.ma (modified) * src/ASM/Status.ma (modified) * src/ASM/StatusProofs.ma (modified) * src/Clight/TypeComparison.ma (modified) * src/Clight/fresh.ma (modified) * src/Clight/label.ma (modified) * src/Clight/test/insertsort.test.ma (modified) * src/Clight/toCminor.ma (modified) * src/Cminor/toRTLabs.ma (modified) * src/ERTL/ERTLToLTL.ma (modified) * src/LIN/LINToASM.ma (modified) * src/LTL/LTLToLIN.ma (modified) * src/RTLabs/RTLabsToRTL.ma (modified) * src/common/Graphs.ma (modified) * src/common/Identifiers.ma (modified) * src/common/PositiveMap.ma (added) * src/common/PreIdentifiers.ma (modified) * src/joint/Erasure.ma (modified) * src/joint/SemanticUtils.ma (modified) * src/joint/TranslateUtils.ma (modified) * src/utilities/binary/positive.ma (modified) * src/utilities/extralib.ma (modified) * src/utilities/extranat.ma (modified) Add type of maps on positive binary numbers, and use them for ... Fri, 14 Oct 2011 17:44:46 GMT sacerdot [1379] * src/LIN/LIN.ma (modified) * src/LIN/LINToASM.ma (modified) * src/LTL/LTLToLIN.ma (modified) Invariant on LIN code removed. In Paris it was decided that a simpler ... Wed, 28 Sep 2011 21:50:32 GMT sacerdot [1282] * src/ERTL/ERTLToLTL.ma (modified) * src/ERTL/Interference.ma (modified) * src/ERTL/build.ma (deleted) * src/ERTL/liveness.ma (modified) * src/LIN/LINToASM.ma (modified) * src/LTL/LTLToLIN.ma (modified) * src/RTL/RTLTailcall.ma (modified) * src/RTL/RTLtoERTL.ma (modified) * src/RTLabs/RTLAbstoRTL.ma (modified) * src/joint/Joint.ma (modified) * src/joint/TranslateUtils.ma (modified) Cosmetic change: names of joint statements/instructions shortened and ... Thu, 22 Sep 2011 10:02:35 GMT sacerdot [1250] * src/ERTL/ERTLToLTL.ma (modified) * src/ERTL/liveness.ma (modified) * src/ERTL/uses.ma (modified) * src/LIN/LIN.ma (modified) * src/LTL/LTLToLIN.ma (modified) * src/RTL/RTLtoERTL.ma (modified) * src/joint/Joint.ma (modified) * src/joint/semantics.ma (modified) * src/utilities/extralib.ma (modified) 1. Sigma types projections moved to utilities/extralib.ma 2. ... Thu, 22 Sep 2011 00:50:44 GMT sacerdot [1246] * src/LIN/LIN.ma (modified) * src/LTL/LTL.ma (modified) * src/LTL/LTLToLIN.ma (modified) * src/joint/Joint.ma (modified) * src/joint/semantics.ma (modified) Yet another change to Joint.ma to accomodate all passes. The ... Wed, 21 Sep 2011 13:56:54 GMT sacerdot [1236] * src/LIN/LIN.ma (modified) * src/LTL/LTLToLIN.ma (modified) * src/joint/Joint.ma (modified) LTLToLin.ma completed (up to a couple of daemons used to provide dead ... Wed, 21 Sep 2011 09:57:20 GMT sacerdot [1233] * src/LIN/LIN.ma (modified) * src/LTL/LTL.ma (modified) * src/LTL/LTLToLIN.ma (modified) * src/RTL/semantics.ma (modified) * src/common/SmallstepExec.ma (modified) * src/joint/Joint.ma (modified) * src/joint/semantics.ma (modified) 1) Ported to Brian's new dependent type for fullexec 2) Universe ... Fri, 16 Sep 2011 16:39:05 GMT sacerdot [1224] * src/Clight/CexecSound.ma (modified) * src/Clight/Csyntax.ma (modified) * src/Clight/SimplifyCasts.ma (modified) * src/Clight/label.ma (modified) * src/Clight/test/search.c.ma (modified) * src/Clight/toCminor.ma (modified) * src/Cminor/initialisation.ma (modified) * src/Cminor/syntax.ma (modified) * src/Cminor/toRTLabs.ma (modified) * src/LIN/LIN.ma (modified) * src/LTL/LTLToLIN.ma (modified) * src/RTLabs/RTLAbstoRTL.ma (modified) * src/RTLabs/syntax.ma (modified) * src/common/AST.ma (modified) * src/common/Globalenvs.ma (modified) * src/common/IntValue.ma (deleted) Type of programs in common/AST made more dependent. In particular, ... Mon, 05 Sep 2011 10:01:58 GMT mulligan [1180] * src/LTL/LTLToLIN.ma (modified) lin to ltl pass complete Fri, 02 Sep 2011 12:51:20 GMT mulligan [1171] * src/ERTL/ERTL.ma (modified) * src/ERTL/ERTLToLTL.ma (modified) * src/LIN/LIN.ma (modified) * src/LTL/LTL.ma (modified) * src/LTL/LTLToLIN.ma (modified) * src/joint/Joint.ma (modified) changes made on claudio's request: changed order of nesting in the ... Fri, 02 Sep 2011 08:35:24 GMT mulligan [1166] * src/ERTL/ERTLToLTL.ma (modified) * src/LIN/LIN.ma (modified) * src/LTL/LTL.ma (modified) * src/LTL/LTLToLIN.ma (modified) * src/joint (added) * src/joint/JointLTLLIN.ma (moved) moved joint ltl lin files into their own directory. more changes to ... Thu, 01 Sep 2011 14:53:01 GMT mulligan [1164] * src/LIN/JointLTLLIN.ma (modified) * src/LIN/LIN.ma (modified) * src/LTL/LTL.ma (modified) * src/LTL/LTLToLIN.ma (modified) ltl to lin working again, more changes to joint syntax Tue, 30 Aug 2011 14:22:54 GMT mulligan [1149] * src/LIN/LINToASM.ma (modified) * src/LTL/LTLToLIN.ma (modified) * src/RTL/RTLtoERTL.ma (modified) * src/RTLabs/RTLAbstoRTL.ma (modified) changes to get everything type checking again after changing names of ... Wed, 24 Aug 2011 16:47:09 GMT mulligan [1111] * src/LTL/LTLToLIN.ma (modified) minor change: marked some possibly dodgy (and very complex) code Wed, 24 Aug 2011 16:45:01 GMT mulligan [1110] * src/ERTL/ERTLToLTL.ma (modified) * src/LIN/JointLTLLIN.ma (modified) * src/LIN/LIN.ma (modified) * src/LTL/LTL.ma (modified) * src/LTL/LTLToLIN.ma (modified) changes to get ltl to lin pass to work properly Mon, 18 Apr 2011 15:32:46 GMT mulligan [759] * src/ERTL/ERTL.ma (modified) * src/ERTL/ERTLToLTL.ma (modified) * src/LTL/LTLToLIN.ma (modified) * src/RTL/RTLtoERTL.ma (modified) More work on the RTL to ERTL pass. Mon, 18 Apr 2011 10:30:53 GMT mulligan [757] * src/ASM/ASM.ma (modified) * src/ASM/Assembly.ma (modified) * src/ASM/I8051.ma (modified) * src/ASM/Interpret.ma (modified) * src/ASM/Status.ma (modified) * src/ERTL/ERTLToLTL.ma (modified) * src/LIN/JointLTLLIN.ma (modified) * src/LIN/LIN.ma (modified) * src/LIN/LINToASM.ma (modified) * src/LTL/LTL.ma (modified) * src/LTL/LTLToLIN.ma (modified) * src/common/AST.ma (modified) * src/common/CostLabel.ma (modified) * src/common/Identifiers.ma (modified) * src/common/Registers.ma (modified) Lots more fixing to get both front and backends using same ... Thu, 14 Apr 2011 15:54:37 GMT mulligan [753] * src/ERTL/ERTL.ma (modified) * src/ERTL/ERTLToLTL.ma (modified) * src/LTL/Branch.ma (deleted) * src/LTL/LTL.ma (modified) * src/LTL/LTLToLIN.ma (modified) * src/common/Identifiers.ma (modified) * src/utilities/BitVectorTrieSet.ma (modified) Work from today. Fri, 01 Apr 2011 14:09:51 GMT mulligan [733] * src/ERTL (added) * src/ERTL/Build.ma (added) * src/ERTL/ERTL.ma (added) * src/ERTL/ERTLToLTL.ma (added) * src/ERTL/Liveness.ma (added) * src/LIN/JointLTLLIN.ma (added) * src/LTL/Branch.ma (added) * src/LTL/LTLToLIN.ma (modified) * src/LTL/LTLToLINI.ma (deleted) * src/utilities/UnionFind.ma (added) Fixed partial commit. Thu, 31 Mar 2011 15:53:16 GMT mulligan [728] * src/LTL/LTLToLIN.ma (modified) * src/LTL/LTLToLINI.ma (modified) * src/common/Graphs.ma (modified) Changes from last two days. Wed, 30 Mar 2011 10:34:25 GMT mulligan [723] * src/CHANGES (modified) * src/LIN/LIN.ma (modified) * src/LIN/LINToASM.ma (modified) * src/LTL/LTL.ma (modified) * src/LTL/LTLToLIN.ma (modified) Added dependent type internalising the invariant that LIN function ... Tue, 29 Mar 2011 16:32:47 GMT mulligan [722] * src/ASM/ASM.ma (modified) * src/LIN/LIN.ma (modified) * src/LIN/LINToASM.ma (modified) * src/LTL/LTL.ma (modified) * src/LTL/LTLToLIN.ma (modified) * src/LTL/LTLToLINI.ma (modified) * src/common/AST.ma (modified) Committing changes from today. Several files do not typecheck. Tue, 29 Mar 2011 12:29:12 GMT mulligan [716] * src/LTL/LTL.ma (modified) * src/LTL/LTLToLIN.ma (modified) * src/LTL/LTLToLINI.ma (added) Finished translating LTL statements to LIN statements. Need to ... Tue, 29 Mar 2011 11:49:57 GMT mulligan [715] * src/ASM/Util.ma (modified) * src/LTL/LTLToLIN.ma (modified) Restored rev from Util as it appears that list reversal is not a part ... Tue, 29 Mar 2011 10:24:45 GMT mulligan [714] * src/ASM/ASM.ma (modified) * src/LIN/LIN.ma (modified) * src/LTL/LTL.ma (modified) * src/LTL/LTLToLIN.ma (added) * src/common/AST.ma (modified) Work on translation from LTL to LIN.