Changeset 733


Ignore:
Timestamp:
Apr 1, 2011, 4:09:51 PM (9 years ago)
Author:
mulligan
Message:

Fixed partial commit.

Location:
src
Files:
8 added
1 deleted
1 edited

Legend:

Unmodified
Added
Removed
  • src/LTL/LTLToLIN.ma

    r728 r733  
    3434    graph_lookup ? g l.
    3535
     36definition 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)).
     40  if marked l2 visited then
     41    〈require lbl required, (Joint_St_Goto ? globals l2) :: generated〉
     42  else
     43   visit globals g required visited generated l2 n.
     44
    3645let rec visit (globals: list Identifier) (g: LTLStatementGraph globals)
    3746              (required: BitVectorTrieSet 16) (visited: BitVectorTrieSet 16)
     
    5665                required in
    5766            let 〈required', generated''〉 ≝
     67             foo l2 visited' required' globals generated'' g n' visit (*
    5868              if marked l2 visited' then
    5969                〈required', (Joint_St_Goto ? globals l2) :: generated''〉
    6070              else
    61                 visit globals g required' visited' generated'' l2 n' in
     71                visit globals g required' visited' generated'' l2 n'*) in
    6272            let required'' ≝ require l1 required' in
    6373              if ¬(marked l1 visited') then
Note: See TracChangeset for help on using the changeset viewer.