Theory SM_LTL

theory SM_LTL
imports LTL.LTL SM_Semantics
begin

  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. *)

end