# # ChangeLog for src/LTL/LTL.ma # # Generated by Trac 1.2 # Apr 23, 2021, 8:39:41 PM Fri, 29 Mar 2013 16:19:53 GMT tranquil [3037] * src/ERTL/ERTL.ma (modified) * src/ERTL/ERTLToLTL.ma (modified) * src/ERTL/liveness.ma (modified) * src/ERTL/uses.ma (modified) * src/LIN/LIN.ma (modified) * src/LIN/joint_LTL_LIN_semantics.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 (modified) * src/joint/joint_semantics.ma (modified) * src/joint/linearise.ma (modified) * src/joint/semanticsUtils.ma (modified) * ADDRESS joint instruction now has also an offset * corrected call ... Tue, 26 Mar 2013 13:01:15 GMT tranquil [2952] * src/ERTL/ERTL.ma (modified) * src/ERTLptr/ERTLptr.ma (modified) * src/LIN/LIN.ma (modified) * src/LTL/LTL.ma (modified) * src/RTL/RTL.ma (modified) * src/joint/Traces.ma (modified) * src/joint/joint_fullexec.ma (modified) * src/joint/joint_semantics.ma (modified) * src/joint/semanticsUtils.ma (modified) * corrected all back-end premains to not pass any arguments to the ... Sun, 24 Mar 2013 10:29:01 GMT tranquil [2946] * src/ERTL/ERTL.ma (modified) * src/ERTL/ERTLToERTLptrAxiom.ma (added) * src/ERTL/ERTL_semantics.ma (modified) * src/ERTL/ERTLtoERTLptrUtils.ma (modified) * src/ERTLptr/ERTLptr.ma (modified) * src/ERTLptr/ERTLptrToLTLAxiom.ma (added) * src/ERTLptr/ERTLptr_semantics.ma (modified) * src/LIN/LIN.ma (modified) * src/LIN/LINToASM.ma (modified) * src/LIN/LINToASMAxiom.ma (added) * src/LIN/LIN_semantics.ma (modified) * src/LTL/LTL.ma (modified) * src/LTL/LTLToLINAxiom.ma (moved) * src/LTL/LTL_semantics.ma (modified) * src/RTL/RTL.ma (modified) * src/RTL/RTLToERTLAxiom.ma (moved) * src/RTL/RTL_overflow_to_unique.ma (added) * src/RTL/RTL_semantics.ma (modified) * src/RTL/RTL_separate_to_overflow.ma (added) * src/RTLabs/RTLabsToRTL.ma (modified) * src/RTLabs/RTLabsToRTLAxiom.ma (moved) * src/compiler.ma (modified) * src/joint/Joint.ma (modified) * src/joint/Traces.ma (modified) * src/joint/TranslateUtils.ma (modified) * src/joint/joint_fullexec.ma (modified) * src/joint/joint_semantics.ma (modified) * src/joint/linearise.ma (modified) * src/joint/semanticsUtils.ma (modified) main novelties: * there is an in-built stack_usage nat in joint ... Thu, 02 Aug 2012 13:18:11 GMT tranquil [2286] * src/ASM/I8051.ma (modified) * src/ASM/Util.ma (modified) * src/ASM/Vector.ma (modified) * src/ERTL/ERTL.ma (modified) * src/ERTL/ERTLToLTL.ma (modified) * src/ERTL/ERTLToLTL_paolo.ma (deleted) * src/ERTL/ERTL_paolo.ma (deleted) * src/ERTL/Interference.ma (modified) * src/ERTL/Interference_paolo.ma (deleted) * src/ERTL/liveness.ma (modified) * src/ERTL/liveness_paolo.ma (deleted) * src/ERTL/semantics.ma (modified) * src/ERTL/semantics_paolo.ma (deleted) * src/LIN/LIN.ma (modified) * src/LIN/LINToASM.ma (modified) * src/LIN/LIN_paolo.ma (deleted) * src/LIN/joint_LTL_LIN.ma (modified) * src/LIN/joint_LTL_LIN_paolo.ma (deleted) * src/LIN/joint_LTL_LIN_semantics.ma (modified) * src/LIN/joint_LTL_LIN_semantics_paolo.ma (deleted) * src/LIN/semantics.ma (modified) * src/LIN/semantics_paolo.ma (deleted) * src/LTL/LTL.ma (modified) * src/LTL/LTLToLIN.ma (modified) * src/LTL/LTLToLIN_paolo.ma (deleted) * src/LTL/LTL_paolo.ma (deleted) * src/LTL/semantics.ma (modified) * src/LTL/semantics_paolo.ma (deleted) * src/RTL/RTL.ma (modified) * src/RTL/RTLTailcall.ma (modified) * src/RTL/RTLTailcall_paolo.ma (deleted) * src/RTL/RTLToERTL.ma (modified) * src/RTL/RTLToERTL_paolo.ma (deleted) * src/RTL/RTL_paolo.ma (deleted) * src/RTL/semantics.ma (modified) * src/RTL/semantics_paolo.ma (deleted) * src/RTLabs/RTLabsToRTL.ma (modified) * src/RTLabs/RTLabsToRTL_paolo.ma (deleted) * src/common/AST.ma (modified) * src/common/BackEndOps.ma (added) * src/common/ByteValues.ma (modified) * src/common/ByteValues_paolo.ma (deleted) * src/common/FrontEndVal.ma (modified) * src/common/Registers.ma (modified) * src/compiler.ma (modified) * src/joint/BEMem.ma (modified) * src/joint/Joint.ma (modified) * src/joint/Joint_paolo.ma (deleted) * src/joint/SemanticUtils.ma (modified) * src/joint/Traces.ma (modified) * src/joint/TranslateUtils.ma (modified) * src/joint/TranslateUtils_paolo.ma (deleted) * src/joint/blocks.ma (modified) * src/joint/linearise.ma (modified) * src/joint/semantics.ma (modified) * src/joint/semanticsUtils_paolo.ma (deleted) * src/joint/semantics_paolo.ma (deleted) * src/utilities/extranat.ma (modified) Big update! * merge of all _paolo variants * reorganised some ... Fri, 14 Oct 2011 17:32:21 GMT sacerdot [1378] * src/LIN/LIN.ma (modified) * src/LIN/joint_LTL_LIN.ma (added) * src/LIN/semantics.ma (modified) * src/LTL/LTL.ma (modified) * src/LTL/semantics.ma (modified) New file LIN/joint_LTL_LIN.ma to factorize out the syntactic ... 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 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 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 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 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 ... 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: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 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. 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 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.