Changeset 1082 for src/LTL/LTL.ma

Timestamp:

Jul 20, 2011, 5:17:38 PM (8 years ago)

Author:

mulligan

Message:

work from today on ertl -> ltl pass

File:

• src/LTL/LTL.ma (modified) (1 diff)

src/LTL/LTL.ma

@@ -11 +11 @@
   ltl_if_luniverse: universe LabelTag;
   ltl_if_runiverse: universe RegisterTag;
-  ltl_if_StackSize: nat;
-  ltl_if_Graph: ltl_statement_graph globals;
-  ltl_if_Entry: label;
-  ltl_if_Exit: label
+  ltl_if_stacksize: nat;
+  ltl_if_graph: ltl_statement_graph globals;
+  ltl_if_entry: Σl: label. lookup ? ? ltl_if_graph l ≠ None ?;
+  ltl_if_exit: Σl: label. lookup ? ? ltl_if_graph l ≠ None ?
 }.