# # ChangeLog for src/LTL # # Generated by Trac 1.2 # Jan 22, 2021, 8:41:19 AM Thu, 06 Oct 2011 20:35:29 GMT sacerdot [1312] * src/ERTL/semantics.ma (modified) * src/LIN/semantics.ma (modified) * src/LTL/semantics.ma (modified) * src/joint/semantics.ma (modified) Type of frame operations (pop_frame/save_frame) generalized to take ... Wed, 05 Oct 2011 22:16:22 GMT sacerdot [1303] * src/ERTL/semantics.ma (modified) * src/LTL/semantics.ma (added) * src/RTL/semantics.ma (modified) * src/joint/semantics.ma (modified) 1. LTL/semantics.ma added (work in progress) 2. init_locals fixed to ... 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 ... Wed, 28 Sep 2011 21:08:37 GMT sacerdot [1281] * src/ERTL/ERTLToLTL.ma (modified) * src/LIN/LIN.ma (modified) * src/LTL/LTL.ma (modified) * src/RTLabs/RTLAbstoRTL.ma (modified) * src/joint/semantics.ma (modified) Porting of all transformation to the joint syntax practically ... Wed, 28 Sep 2011 00:43:37 GMT sacerdot [1280] * src/ERTL/ERTL.ma (modified) * src/LTL/LTL.ma (modified) * src/RTL/RTL.ma (modified) * src/RTL/RTLtoERTL.ma (modified) * src/RTLabs/RTLAbstoRTL.ma (modified) * src/joint/Joint.ma (modified) * src/joint/TranslateUtils.ma (added) Some progress in the porting of RTLAbstoRTL to the joint syntax: 1) ... Mon, 26 Sep 2011 14:24:32 GMT mulligan [1271] * src/ERTL/ERTLToLTL.ma (modified) * src/ERTL/liveness.ma (modified) * src/ERTL/uses.ma (modified) * src/LTL/LTL.ma (modified) * src/joint/Joint.ma (modified) finished, kind of Mon, 26 Sep 2011 13:59:28 GMT sacerdot [1270] * src/ERTL/ERTL.ma (modified) * src/LIN/LIN.ma (modified) * src/LIN/LINToASM.ma (modified) * src/LTL/LTL.ma (modified) * src/RTL/RTL.ma (modified) * src/RTL/RTLTailcall.ma (modified) * src/RTL/RTLtoERTL.ma (modified) * src/joint/Joint.ma (modified) Making RTL syntax an instance of Joint. Mon, 26 Sep 2011 13:06:35 GMT sacerdot [1269] * src/ERTL/ERTL.ma (modified) * src/LTL/LTL.ma (modified) Useless include removed. Thu, 22 Sep 2011 12:49:18 GMT sacerdot [1252] * src/ERTL/ERTL.ma (modified) * src/LTL/LTL.ma (modified) * src/RTL/RTLtoERTL.ma (modified) * src/joint/Joint.ma (modified) graph_params added to joint/Joint.ma, together with useful common ... 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, ... Fri, 16 Sep 2011 09:02:23 GMT sacerdot [1222] * src/LTL/LTL.ma (modified) LTL fully ported to the joint syntax. Mon, 05 Sep 2011 11:31:54 GMT mulligan [1183] * src/ERTL/ERTL.ma (modified) * src/LIN/LIN.ma (modified) * src/LTL/LTL.ma (modified) removed parameterised label types in the three lowest level languages Mon, 05 Sep 2011 10:01:58 GMT mulligan [1180] * src/LTL/LTLToLIN.ma (modified) lin to ltl pass complete Mon, 05 Sep 2011 09:58:58 GMT mulligan [1179] * src/ERTL/ERTLToLTL.ma (modified) * src/LIN/LIN.ma (modified) * src/LIN/LINToASM.ma (modified) * src/LTL/LTL.ma (modified) changes to ertl, ltl and lin to use new notion of joint params. ertl ... 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 09:36:15 GMT sacerdot [1168] * src/ERTL/ERTL.ma (modified) * src/ERTL/ERTLToLTL.ma (modified) * src/LIN/LIN.ma (modified) * src/LIN/LINToASM.ma (modified) * src/LTL/LTL.ma (modified) Joint statements parameterized over a record. 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 Thu, 01 Sep 2011 14:23:42 GMT mulligan [1163] * src/ERTL/ERTL.ma (modified) * src/ERTL/ERTLToLTL.ma (modified) * src/ERTL/semantics.ma (modified) * src/LIN/JointLTLLIN.ma (modified) * src/LIN/LIN.ma (modified) * src/LTL/LTL.ma (modified) even more streamlining and fixes to get things type checking Wed, 31 Aug 2011 16:24:03 GMT mulligan [1161] * src/ASM/Util.ma (modified) * src/ERTL/ERTL.ma (modified) * src/ERTL/ERTLToLTL.ma (modified) * src/ERTL/semantics.ma (modified) * src/LIN/JointLTLLIN.ma (modified) * src/LTL/LTL.ma (modified) changes from today: merged ertl, ltl and lin into one datatype to ... 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 ... Mon, 29 Aug 2011 15:30:25 GMT mulligan [1132] * src/LIN/JointLTLLIN.ma (modified) * src/LIN/LIN.ma (modified) * src/LTL/LTL.ma (modified) reunified ltl and lin instruction type, removing lifting in ltl and ... 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 Wed, 27 Jul 2011 15:50:25 GMT mulligan [1089] * src/ASM/I8051.ma (modified) * src/LIN/JointLTLLIN.ma (modified) * src/LTL/LTL.ma (modified) * src/RTL/RTL.ma (modified) * src/RTL/RTLinterpret.ma (added) more changes from earlier in the week Wed, 20 Jul 2011 15:17:38 GMT mulligan [1082] * src/ERTL/ERTL.ma (modified) * src/ERTL/ERTLToLTL.ma (modified) * src/ERTL/ERTLToLTLI.ma (added) * src/ERTL/Liveness.ma (modified) * src/ERTL/Uses.ma (modified) * src/LIN/JointLTLLIN.ma (modified) * src/LTL/LTL.ma (modified) * src/common/Graphs.ma (modified) work from today on ertl -> ltl pass 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. Tue, 29 Mar 2011 09:48:33 GMT mulligan [713] * src/LTL (added) * src/LTL/LTL.ma (added) Commit of initial LTL files.