Changeset 753 for src/LTL


Ignore:
Timestamp:
Apr 14, 2011, 5:54:37 PM (9 years ago)
Author:
mulligan
Message:

Work from today.

Location:
src/LTL
Files:
1 deleted
2 edited

Legend:

Unmodified
Added
Removed
  • src/LTL/LTL.ma

    r723 r753  
    2121  | LTL_Fu_ExternalFunction: ExternalFunction → LTLFunctionDefinition globals.
    2222 
    23 record LTLProgram (globals: list Identifier): Type[0] ≝
     23record LTLProgram (globals: list (Identifier × nat)): Type[0] ≝
    2424{
    25   LTL_Pr_Vars: list (Identifier × nat); (* 2nd component = size *)
    26   LTL_Pr_Funs: list (Identifier × (LTLFunctionDefinition globals));
     25  LTL_Pr_Funs: list (Identifier × (LTLFunctionDefinition (map ? ? \fst globals)));
    2726  LTL_Pr_Main: option Identifier
    2827}.
  • src/LTL/LTLToLIN.ma

    r733 r753  
    33include "utilities/BitVectorTrieSet.ma".
    44include "common/Graphs.ma".
     5
     6axiom LTLTag: String.
    57
    68definition translate_statement: ∀globals. LTLStatement globals → PreLINStatement globals ≝
     
    2628  λl: Identifier.
    2729  λg: BitVectorTrieSet 16.
    28     set_member ? l g.   
     30    set_member ? l g.
     31   
     32definition graph_lookup ≝
     33  λglobals.
     34  λl: Identifier.
     35  λg: LTLStatementGraph globals.
     36    lookup LabelTag (LTLStatement globals) g (an_identifier LabelTag l).
    2937   
    3038definition fetch: ∀globals: list Identifier. Identifier → LTLStatementGraph globals → option (LTLStatement globals) ≝
     
    3240  λl: Identifier.
    3341  λg: LTLStatementGraph globals.
    34     graph_lookup ? g l.
     42    graph_lookup globals l g.
    3543
    36 definition foo ≝ λl2,visited,required,globals,generated,g,n.
    37  λvisit:∀globals: list Identifier.∀g: LTLStatementGraph globals.∀required: BitVectorTrieSet 16.
    38   ∀visited: BitVectorTrieSet 16.∀generated: list (PreLINStatement globals).∀l: Identifier.
    39   ∀n: nat.BitVectorTrieSet 16 × (list (PreLINStatement globals)).
     44definition foo ≝
     45  λl2, visited, required, globals, generated, g, n.
     46  λvisit:
     47  ∀globals: list Identifier.
     48  ∀g: LTLStatementGraph globals.
     49  ∀required: BitVectorTrieSet 16.
     50  ∀visited: BitVectorTrieSet 16.
     51  ∀generated: list (PreLINStatement globals).
     52  ∀l: Identifier.
     53  ∀n: nat.
     54    BitVectorTrieSet 16 × (list (PreLINStatement globals)).
    4055  if marked l2 visited then
    41     〈require lbl required, (Joint_St_Goto ? globals l2) :: generated〉
     56    〈require l2 required, (Joint_St_Goto ? globals l2) :: generated〉
    4257  else
    4358   visit globals g required visited generated l2 n.
Note: See TracChangeset for help on using the changeset viewer.