Lines Matching defs:model
2 (* this contains all info about the model, including the properties to be checked, and th eventual results *)
21 type model = {init: term option,
37 fun get_name (m:model) = #name(m)
38 fun get_init (m:model) = valOf (#init(m))
39 fun get_trans (m:model) = valOf (#trans(m))
40 fun get_flag_ric (m:model) = valOf (#ric(m))
41 fun get_vord (m:model) = #vord(m)
42 fun get_state (m:model) = #state(m)
43 fun get_props (m:model) = valOf (#props(m))
44 fun get_results (m:model) = #results(m)
45 fun get_ic (m:model) = #ic(m)
47 fun get_flag_abs (m:model) = #abs (#flags m) (*if true, hc will try to do abstraction if possible and worthwhile; otherwise no abs *)
50 fun set_name nm (m:model) =
55 fun set_init i (m:model) =
60 fun set_flag_ric r (m:model) =
64 fun set_vord v (m:model) = (* no point in any vetting here since it is easy to get around *)
68 fun set_state s (m:model) = (* no point in any vetting here since it is easy to get around *)
72 fun set_trans t (m:model) =
91 fun set_props p (m:model) =
113 fun set_results res (m:model) =
117 fun set_ic ic (m:model) =
121 fun set_flag_abs abs (m:model) =
126 fun add_trans t (m:model) = (*FIXME: expose this (need more infrastructure to handle invalidation of results since model has changed) *)
135 fun add_prop p (m:model) =
151 fun prove_model (m:model) =