Changeset 728 for src/LTL


Ignore:
Timestamp:
Mar 31, 2011, 5:53:16 PM (9 years ago)
Author:
mulligan
Message:

Changes from last two days.

Location:
src/LTL
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/LTL/LTLToLIN.ma

    r723 r728  
    11include "LTL/LTL.ma".
    22include "LIN/LIN.ma".
     3include "utilities/BitVectorTrieSet.ma".
     4include "common/Graphs.ma".
    35
    46definition translate_statement: ∀globals. LTLStatement globals → PreLINStatement globals ≝
     
    810    [ Joint_St_Return ⇒ Joint_St_Return ? globals
    911    | Joint_St_Sequential instr _ ⇒ Joint_St_Sequential ? globals instr it
     12    | Joint_St_Goto lbl ⇒ Joint_St_Goto ? globals lbl
    1013    ].
     14   
     15definition require: Identifier → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝
     16  λl: Identifier.
     17  λg: BitVectorTrieSet 16.
     18    set_insert ? l g.
     19   
     20definition mark: Identifier → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝
     21  λl: Identifier.
     22  λg: BitVectorTrieSet 16.
     23    set_insert ? l g.
     24   
     25definition marked: Identifier → BitVectorTrieSet 16 → bool ≝
     26  λl: Identifier.
     27  λg: BitVectorTrieSet 16.
     28    set_member ? l g.   
     29   
     30definition fetch: ∀globals: list Identifier. Identifier → LTLStatementGraph globals → option (LTLStatement globals) ≝
     31  λglobals: list Identifier.
     32  λl: Identifier.
     33  λg: LTLStatementGraph globals.
     34    graph_lookup ? g l.
     35
     36let rec visit (globals: list Identifier) (g: LTLStatementGraph globals)
     37              (required: BitVectorTrieSet 16) (visited: BitVectorTrieSet 16)
     38              (generated: list (PreLINStatement globals)) (l: Identifier) (n: nat) on n: BitVectorTrieSet 16 × (list (PreLINStatement globals)) ≝
     39  match n with
     40  [ O ⇒ 〈required, generated〉
     41  | S n' ⇒
     42    let visited' ≝ mark l visited in
     43    match fetch globals l g with
     44    [ None ⇒ 〈required, generated〉 (* dpm: correct? *)
     45    | Some statement ⇒
     46      let translated_statement ≝ translate_statement globals statement in
     47      let generated'' ≝ translated_statement :: generated in
     48      match statement with
     49      [ Joint_St_Sequential instr l2 ⇒
     50        match instr with
     51        [ Joint_Instr_CondAcc l1 ⇒
     52            let required' ≝
     53              if marked l2 visited' then
     54                require l2 required
     55              else
     56                required in
     57            let 〈required', generated''〉 ≝
     58              if marked l2 visited' then
     59                〈required', (Joint_St_Goto ? globals l2) :: generated''〉
     60              else
     61                visit globals g required' visited' generated'' l2 n' in
     62            let required'' ≝ require l1 required' in
     63              if ¬(marked l1 visited') then
     64                visit globals g required'' visited' generated'' l1 n'
     65              else
     66                〈required', generated''〉
     67        | _ ⇒
     68          let required' ≝
     69            if marked l2 visited' then
     70              require l2 required
     71            else
     72              required in
     73          if marked l2 visited' then
     74            〈required', Joint_St_Goto ? globals l2 :: generated''〉
     75          else
     76            visit globals g required' visited' generated'' l2 n'
     77        ]
     78      | Joint_St_Goto lbl ⇒
     79        let required' ≝
     80          if marked lbl visited' then
     81            require lbl required
     82          else
     83            required in
     84        if marked lbl visited' then
     85          〈required', (Joint_St_Goto ? globals lbl) :: generated''〉
     86        else
     87          visit globals g required' visited' generated'' lbl n'
     88      | Joint_St_Return ⇒ 〈required, generated''〉 (* dpm: correct? *)
     89      ]
     90    ]
     91  ].
     92
     93(*
     94definition translate_graph ≝
     95  λglobals: list Identifier.
     96  λg: LTLStatementGraph globals.
     97  λentry: Identifier.
     98    let visited ≝ set_empty ? in
     99    let required ≝ set_insert ? entry (set_empty ?) in
     100    let 〈required', translated〉 ≝ visit globals g required visited [ ] entry in
     101    let reversed ≝ rev ? translated in
     102      filter (λs: PreLINStatement globals. ?) reversed.
     103*)
  • src/LTL/LTLToLINI.ma

    r722 r728  
    1 include "common/Graphs.ma".
    2 include "LTL/LTL.ma".
    3 
    4 definition fetch: ∀globals. LTLStatementGraph globals → label → option (LTLStatement globals) ≝
    5   λglobals: list Identifier.
    6   λgraph: LTLStatementGraph globals.
    7   λl: label.
    8     graph_lookup ? graph l.
    9    
    10 definition generate: ∀globals. LTLStatement globals → list (LTLStatement globals) → list (LTLStatement globals) ≝
    11   λglobals.
    12   λstatement.
    13   λstatements.
    14     statement :: statements.
Note: See TracChangeset for help on using the changeset viewer.