Changeset 1250 for src/LTL


Ignore:
Timestamp:
Sep 22, 2011, 12:02:35 PM (8 years ago)
Author:
sacerdot
Message:
  1. Sigma types projections moved to utilities/extralib.ma
  2. Extended statement turned into extended instructions, decreasing the amount of code in the translations
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LTL/LTLToLIN.ma

    r1246 r1250  
    88  λs: ltl_statement globals.
    99  match s with
    10   [ joint_st_return ⇒ joint_st_return
     10  [ joint_st_return ⇒ joint_st_return ??
    1111  | joint_st_sequential instr lbl ⇒ joint_st_sequential … instr it
    12   | joint_st_goto l ⇒ joint_st_goto … l
    13   | joint_st_extension ext ⇒ joint_st_extension lin_params_ … ext
     12  | joint_st_goto l ⇒ joint_st_goto lin_params_ globals l
    1413  ].
    1514
     
    4948         | _ ⇒ visit globals g required visited' generated' l2 n']
    5049     | joint_st_return ⇒ 〈required, generated'〉
    51      | joint_st_goto l2 ⇒ visit globals g required visited' generated' l2 n'
    52      | joint_st_extension ext ⇒ ⊥ ]]].
    53 [3: @ext
    54 |1,2: @daemon (*CSC: impossible cases, use more dependent types *) ]
     50     | joint_st_goto l2 ⇒ visit globals g required visited' generated' l2 n']]].
     51[1,2: @daemon (*CSC: impossible cases, use more dependent types *) ]
    5552qed.
    5653
Note: See TracChangeset for help on using the changeset viewer.