Changeset 1324 for src/LTL/semantics.ma


Ignore:
Timestamp:
Oct 7, 2011, 3:32:07 PM (9 years ago)
Author:
sacerdot
Message:

The semantics of extended statements must also consider the label since
the program counter is not automatically incremented
(because of cond instructions :-(

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/LTL/semantics.ma

    r1312 r1324  
    3535axiom ltl_set_result: list val → state ltl_sem_params → res (state ltl_sem_params).
    3636
    37 definition ltl_exec_extended: ∀globals. genv globals (ltl_params globals) → False → state ltl_sem_params → IO io_out io_in (trace × (state ltl_sem_params))
     37definition ltl_exec_extended: ∀globals. genv globals (ltl_params globals) → False → label → state ltl_sem_params → IO io_out io_in (trace × (state ltl_sem_params))
    3838 ≝ λglobals,ge,abs. ⊥.
    3939@abs qed.
Note: See TracChangeset for help on using the changeset viewer.