Changeset 1274 for src/ERTL


Ignore:
Timestamp:
Sep 26, 2011, 5:58:21 PM (8 years ago)
Author:
mulligan
Message:

starting removing axioms from adts and giving them proper implementations

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToLTL.ma

    r1271 r1274  
    501501      ]) (joint_if_code globals (ertl_params globals) int_fun) 〈graph, joint_if_luniverse … int_fun〉
    502502  in
    503     mk_joint_internal_function globals (ltl_params globals)
    504       luniv (joint_if_runiverse … int_fun)
    505         it it it (joint_if_stacksize … int_fun)
    506           graph ? ?.
    507   cases daemon (* XXX *)
     503    match joint_if_entry … int_fun with
     504    [ dp entry_label entry_label_prf ⇒
     505      match joint_if_exit … int_fun with
     506      [ dp exit_label exit_label_prf ⇒
     507          mk_joint_internal_function globals (ltl_params globals)
     508            luniv (joint_if_runiverse … int_fun)
     509              it it it (joint_if_stacksize … int_fun)
     510                graph ? ?
     511      ]
     512    ].
     513  [1: %
     514    [1: @entry_label
     515    |2: cases daemon (* XXX *)
     516    ]
     517  |2: %
     518    [1: @exit_label
     519    |2: cases daemon (* XXX *)
     520    ]
     521  ]
    508522qed.
    509523
    510 definition ertl_to_ltl : ertl_program → ltl_program ≝
    511  λp. transform_program … p (transf_fundef … (translate_internal …)).
     524definition ertl_to_ltl: ertl_program → ltl_program ≝
     525  λp.
     526    transform_program … p (transf_fundef … (translate_internal …)).
Note: See TracChangeset for help on using the changeset viewer.