Theory SM_LTL

theory SM_LTL
imports LTL.LTL SM_Semantics

  definition test_aprop :: "exp  valuation  bool"
    where "test_aprop e s  case eval_exp e ( local_state.variables = Map.empty ,
       global_state.variables = s ) of None  False | Some v  bool_of_val v"

  definition sm_props :: "valuation  exp set"
    where "sm_props s  {e. test_aprop e s}"

  definition ap_accept :: "program  (nat  exp set)  bool"
    where "ap_accept prog w   w'. ref_accept prog w'  w = sm_props  global_state.variables  w'"
  (* TODO: Can we get rid of the 
    distribution of global_state.variables here, 
    and global_config.state in the SM_Semantics reference point? *)
  (* TODO: also think about separating types for global/local/undecided stuff, or at least
    factor this part out of the various types of expressions, cmds, actions, etc. *)