Changeset 1171 for src/LTL


Ignore:
Timestamp:
Sep 2, 2011, 2:51:20 PM (8 years ago)
Author:
mulligan
Message:

changes made on claudio's request: changed order of nesting in the joint-ertl statements to make the semantics easier to write. big changes required...

Location:
src/LTL
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/LTL/LTL.ma

    r1168 r1171  
    66 mk_params unit unit unit unit registers_move Register.
    77
    8 definition ltl_statement ≝ λglobals: list ident. joint_statement label ltl_params globals.
     8definition ltl_statement ≝ λglobals: list ident. joint_statement label unit ltl_params globals.
    99 
    1010definition ltl_statement_graph ≝ λglobals. graph (ltl_statement globals).
  • src/LTL/LTLToLIN.ma

    r1166 r1171  
    1010  λs: ltl_statement globals.
    1111  match s with
    12   [ ltl_st_lift_joint joint ⇒
    13     match joint with
    14     [ joint_st_return ⇒ joint_st_return … globals
    15     | joint_st_sequential instr _ ⇒ joint_st_sequential … globals instr it
    16     | joint_st_goto l ⇒ joint_st_goto … globals l
    17     ]
     12  [ joint_st_return ⇒ joint_st_return … globals
     13  | joint_st_sequential instr _ ⇒ joint_st_sequential … globals instr it
     14  | joint_st_goto l ⇒ joint_st_goto … globals l
     15  | joint_st_extension ext ⇒ joint_st_extension … ext
    1816  ].
    1917   
     
    8179      let generated'' ≝ translated_statement :: generated in
    8280      match statement with
    83       [ ltl_st_lift_joint joint ⇒
    84         match joint with
    85         [ joint_st_sequential instr l2 ⇒
    86           match instr with
    87           [ joint_instr_cond acc_a_reg l1 ⇒
    88                 let required' ≝
    89                   if marked l2 visited' then
    90                     require l2 required
    91                   else
    92                     required in
    93                 let 〈required', generated''〉 ≝
    94                  foo l2 visited' required' globals generated'' g n' visit (*
    95                   if marked l2 visited' then
    96                     〈required', (Joint_St_Goto ? globals l2) :: generated''〉
    97                   else
    98                     visit globals g required' visited' generated'' l2 n'*) in
    99                 let required'' ≝ require l1 required' in
    100                   if ¬(marked l1 visited') then
    101                     visit globals g required'' visited' generated'' l1 n'
    102                   else
    103                     〈required', generated''〉
    104             | _ ⇒
     81      [ joint_st_sequential instr l2 ⇒
     82        match instr with
     83        [ joint_instr_cond acc_a_reg l1 ⇒
    10584              let required' ≝
    10685                if marked l2 visited' then
     
    10887                else
    10988                  required in
     89              let 〈required', generated''〉 ≝
     90               foo l2 visited' required' globals generated'' g n' visit (*
     91                if marked l2 visited' then
     92                  〈required', (Joint_St_Goto ? globals l2) :: generated''〉
     93                else
     94                  visit globals g required' visited' generated'' l2 n'*) in
     95              let required'' ≝ require l1 required' in
     96                if ¬(marked l1 visited') then
     97                  visit globals g required'' visited' generated'' l1 n'
     98                else
     99                  〈required', generated''〉
     100          | _ ⇒
     101            let required' ≝
    110102              if marked l2 visited' then
    111                 〈required', joint_st_goto … globals l2 :: generated''〉
     103                require l2 required
    112104              else
    113                 visit globals g required' visited' generated'' l2 n'
    114             ]
    115           | joint_st_return ⇒ 〈required, generated''〉 (* dpm: correct? *)
    116       | joint_st_goto l ⇒
    117         let required' ≝
    118            if marked l visited' then
    119              require l required
    120            else
    121              required
    122          in
    123            if marked l visited' then
    124              〈required', joint_st_goto … globals l :: generated''〉
    125            else
    126              visit globals g required' visited' generated'' l n'
    127       ]
     105                required in
     106            if marked l2 visited' then
     107              〈required', joint_st_goto … globals l2 :: generated''〉
     108            else
     109              visit globals g required' visited' generated'' l2 n'
     110          ]
     111    | joint_st_return ⇒ 〈required, generated''〉 (* dpm: correct? *)
     112    | joint_st_goto l ⇒
     113      let required' ≝
     114        if marked l visited' then
     115         require l required
     116        else
     117         required
     118      in
     119        if marked l visited' then
     120          〈required', joint_st_goto … globals l :: generated''〉
     121        else
     122          visit globals g required' visited' generated'' l n'
     123    | joint_st_extension ext ⇒ 〈required, generated〉
    128124    ]
    129125  ]
Note: See TracChangeset for help on using the changeset viewer.