# # ChangeLog for src/ERTL/ERTL.ma # # Generated by Trac 1.2 # Mar 4, 2021, 4:44:58 AM Thu, 01 Sep 2011 15:18:33 GMT mulligan [1165] * src/ERTL/ERTL.ma (modified) * src/ERTL/ERTLToLTL.ma (modified) more changes 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 10:08:25 GMT mulligan [1138] * src/ERTL/ERTL.ma (modified) * src/ERTL/ERTLToLTLI.ma (modified) * src/RTL/RTLtoERTL.ma (modified) * src/RTLabs/RTLAbstoRTL.ma (modified) merged ertl_st_opaccs_a and ertl_st_opaccs_b into each other Mon, 29 Aug 2011 16:01:41 GMT mulligan [1136] * src/ERTL/ERTL.ma (modified) * src/ERTL/ERTLToLTLI.ma (modified) fixed ertl pass Mon, 29 Aug 2011 15:19:31 GMT mulligan [1131] * src/ERTL/ERTL.ma (modified) * src/ERTL/ERTLToLTLI.ma (modified) * src/RTL/RTLtoERTL.ma (modified) changes to syntax of ertl: removed ertl_st_addr_l and ertl_st_addr_h ... Wed, 24 Aug 2011 12:43:58 GMT mulligan [1107] * src/ERTL/ERTL.ma (modified) * src/ERTL/liveness.ma (modified) * src/RTL/RTLtoERTL.ma (modified) got rtl-ertl pass working again Thu, 21 Jul 2011 15:00:47 GMT mulligan [1084] * src/ERTL/ERTL.ma (modified) * src/ERTL/ERTLToLTL.ma (modified) * src/ERTL/ERTLToLTLI.ma (modified) more added on ertl pass: not sure how much should be axiomatised wrt ... 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 Tue, 19 Jul 2011 10:23:32 GMT mulligan [1077] * src/ERTL/ERTL.ma (modified) * src/RTL/RTLtoERTL.ma (modified) * src/RTLabs/RTLAbstoRTL.ma (modified) * src/common/Graphs.ma (modified) * src/common/Identifiers.ma (modified) ack, dependent types are scary Fri, 15 Jul 2011 12:40:40 GMT mulligan [1071] * src/ASM/I8051.ma (modified) * src/ASM/Util.ma (modified) * src/ERTL/ERTL.ma (modified) * src/RTL/RTL.ma (modified) * src/RTL/RTLtoERTL.ma (modified) * src/RTLabs/RTLAbstoRTL.ma (modified) * src/RTLabs/syntax.ma (modified) changes the specific form that the added proofs take to use None, not ... Fri, 03 Jun 2011 15:35:27 GMT campbell [878] * src/Cminor/syntax.ma (modified) * src/ERTL/ERTL.ma (modified) * src/LIN/LIN.ma (modified) * src/RTL/RTL.ma (modified) * src/RTLabs/import.ma (modified) * src/RTLabs/syntax.ma (modified) Removal of manually inserted record projections. Fri, 29 Apr 2011 11:36:35 GMT mulligan [783] * src/ERTL/ERTL.ma (modified) * src/RTL/RTL.ma (modified) * src/RTL/RTLtoERTL.ma (modified) rtl to ertl pass complete (modulo some straightforward axioms that ... Thu, 28 Apr 2011 15:36:33 GMT mulligan [782] * src/ASM/BitVectorTrie.ma (modified) * src/ASM/Util.ma (modified) * src/ERTL/ERTL.ma (modified) * src/RTL/RTL.ma (modified) * src/RTL/RTLtoERTL.ma (modified) * src/common/Identifiers.ma (modified) * src/utilities/RegisterSet.ma (modified) More work on rtl-ertl pass from today, plus resolved conflict. Wed, 27 Apr 2011 15:25:26 GMT mulligan [777] * src/ASM/I8051.ma (modified) * src/ASM/RegisterSet.ma (added) * src/ASM/Util.ma (modified) * src/ERTL/ERTL.ma (modified) * src/ERTL/Uses.ma (modified) * src/RTL/RTLtoERTL.ma (modified) * src/common/Registers.ma (modified) Lots of work on RTL to ERTL pass from today. 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. Fri, 15 Apr 2011 15:47:32 GMT mulligan [756] * src/ERTL/Build.ma (modified) * src/ERTL/ERTL.ma (modified) * src/ERTL/Liveness.ma (modified) * src/ERTL/Uses.ma (modified) * src/RTL/RTL.ma (modified) * src/RTL/RTLtoERTL.ma (added) Made a start on RTL. Renaming in ERTL and below to move closer to ... 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, 08 Apr 2011 08:15:30 GMT mulligan [745] * src/ERTL/ERTL.ma (modified) * src/ERTL/ERTLToLTL.ma (modified) * src/ERTL/Liveness.ma (modified) * src/ERTL/Uses.ma (added) Changes from yesterday. Slowly implementing the functorized ... Fri, 01 Apr 2011 16:12:57 GMT mulligan [735] * src/ERTL/ERTL.ma (modified) * src/ERTL/Liveness.ma (modified) * src/utilities/IdentifierTools.ma (modified) Changes 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.