Domain model
The domain model is the shared foundation for all scenarios and analysis.
It captures:
- the state/action types
- predicates over state/action
- transitions that define behavior
- auxiliary logic
Base model
speclogician ch base-edit --src "type state = { x : int }\ntype action = int"Predicates
State predicate example:
speclogician ch pred-add --pred-type state --pred-name pred_eq_ten --pred-src "s.x = 10"Action predicate example:
speclogician ch pred-add --pred-type action --pred-name act_gt_x --pred-src "a > s.x"Transitions
speclogician ch trans-add \
--trans-name step1 \
--trans-src "let step1 (s: state) (a: action) : state = { x = s.x + a }"