CLI guide

SpecLogician uses typed “change” commands:

speclogician ch ... applies a change and creates a new state instance
speclogician view ... inspects state components

Change commands (examples)

Base model

speclogician ch base-edit --src "type state = int\ntype action = int"
speclogician ch base-edit --file ./base.iml

Predicates

speclogician ch pred-add --pred-type state --pred-name pred_eq_ten --pred-src "s = 10"
speclogician ch pred-edit --pred-name pred_eq_ten --pred-src "s = 11"
speclogician ch pred-remove --pred-name pred_eq_ten

Transitions

speclogician ch trans-add --trans-name step1 --trans-src "let step1 (s: state) (a: action) : state = s + a"
speclogician ch trans-edit --trans-name step1 --trans-src "let step1 (s: state) (a: action) : state = s + (a + 1)"
speclogician ch trans-remove --trans-name step1

Scenarios

speclogician ch scenario-add sc1 --given pred_eq_ten --when act_gt_state --then step1
speclogician ch scenario-edit sc1 --given "+pred_ne_ten,-pred_eq_ten"
speclogician ch scenario-remove sc1