Ignore:
Timestamp:
Apr 15, 2013, 4:31:50 PM (7 years ago)
Author:
tranquil
Message:
  • removed sigma types from traces of intensional events
  • completed correctness.ma using axiom files, a single daemon remains
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToLTLAxiom.ma

    r3096 r3145  
    66include "common/AssocList.ma".
    77
    8 (* Inefficient, replace with Trie lookup *)
    9 definition lookup_stack_cost ≝
    10  λp.λid : ident.
    11   assoc_list_lookup ? ℕ id (eq_identifier …) p.
    12 
    138axiom ERTLToLTL_ok :
    149∀fix_comp : fixpoint_computer.
     
    1712let 〈p_out, m, n〉 ≝ ertl_to_ltl fix_comp colour p_in in
    1813(* what should we do with n? *)
    19 let stacksizes ≝ lookup_stack_cost m in
     14let stacksizes ≝ stack_sizes m in
    2015∀init_in.make_initial_state
    2116  (mk_prog_params ERTL_semantics p_in stacksizes) = OK … init_in →
Note: See TracChangeset for help on using the changeset viewer.