I'm trying to implement a state machine in TLA+, and I encountered a few questions when checking it with TLC.
I think there might be some problems in my spec,and you might not understand what I'm implementing in spec.So I want to explain what I'm doing first.
First,it will read two inputs.In_sentence_seq stand for future command sequence,changing the state of the state machine.In_layer_name stand for input data,and will be used in some specfic states later.And they will turn into variable in_seq and layer_set,maybe after some processes though.
Then,the state machine starts with Init,and then change its state(cur_state) by state_changer when in_seq not empty, or by state_stabler when in_seq empty.After that, do something(meaning only one in actions derived_def_global,rule_head,derived_def_rule,check_statement) depend on cur_state or do nothing if cur_state equals 0.After that,change state by state_changer or state_stabler again.And the state machine will repeat the change state->do something or nothing process again and again.
My spec is written in this way:
----------------------------- MODULE Parser -----------------------------
EXTENDS Integers,Naturals,Reals,Sequences
CONSTANTS in_sentence_seq,in_layer_names
ASSUME /\ in_sentence_seq \in Seq(1..5)
/\ in_layer_names \subseteq 0..10
VARIABLES in_seq,layer_set,cur_state,cur_scope,rule_nums,layer_connection_set
vars == << in_seq,layer_set,cur_state,cur_scope,rule_nums,layer_connection_set >>
layer_range == {{x,y}:x \in 0..10,y \in -1..10}
layer_connection_range == {<<x,y,z>>: x \in layer_range , y \in layer_range , z \in layer_range}
TypeOK == /\ in_seq \in Seq(1..5)
/\ layer_set \subseteq layer_range
/\ cur_state \in 0..5
/\ cur_scope \in -1..10
/\ rule_nums \in 0..10
/\ layer_connection_set \subseteq layer_connection_range
Init == /\ in_seq = in_sentence_seq
/\ layer_set = {{x,y}:x \in in_layer_names,y \in {-1}}
/\ cur_state = 0
/\ cur_scope = -1
/\ rule_nums = 0
/\ layer_connection_set = {}
state_changer == /\ Len(in_seq) >= 1
/\ cur_state' = Head(in_seq)
/\ in_seq' = Tail(in_seq)
/\ UNCHANGED << layer_set,cur_scope,rule_nums,layer_connection_set >>
state_stabler == /\ Len(in_seq) = 0
/\ cur_state'= 0
/\ UNCHANGED << in_seq,layer_set,cur_scope,rule_nums,layer_connection_set >>
scope_changer == /\ cur_state = 5
/\ cur_scope' = -1
/\ UNCHANGED << in_seq,layer_set,cur_state,rule_nums,layer_connection_set >>
derived_def_global ==
LET
temp_num == CHOOSE x \in 0..10: {x,-1} \notin layer_set
temp == {temp_num,-1}
temp_one_num == CHOOSE x \in 0..10: {x,-1} \in layer_set
temp_two_num == CHOOSE x \in 0..10: {x,-1} \in (layer_set\{temp})
temp_one == {temp_one_num,-1}
temp_two == {temp_two_num,-1}
IN
/\ cur_state = 1
/\ cur_scope = -1
/\ layer_set' = layer_set \union temp
/\ layer_connection_set' = layer_connection_set \union {<<temp_one,temp_two,temp>>}
/\ UNCHANGED << in_seq,cur_state,cur_scope,rule_nums >>
rule_head == /\ cur_state = 2
/\ cur_scope' = drc_rule_nums
/\ rule_nums' = rule_nums + 1
/\ UNCHANGED << in_seq,layer_set,cur_state,layer_connection_set >>
derived_def_rule ==
LET
temp_num == CHOOSE x \in 0..10: {x,rule_nums} \notin layer_set
temp_one == CHOOSE z \in {{x,y}: x \in 0..10, y \in {-1,rule_nums}}: z \in layer_set
temp_two == CHOOSE z \in {{x,y}: x \in 0..10, y \in {-1,rule_nums}}: z \in (layer_set\{temp_one})
temp == {temp_num,rule_nums}
IN
/\ cur_state = 3
/\ layer_set' = layer_set \union temp
/\ layer_connection_set' = layer_connection_set \union {<<temp_one,temp_two,temp>>}
/\ UNCHANGED << in_seq,cur_state,cur_scope,rule_nums >>
check_statement ==
LET
temp_num == CHOOSE x \in 0..10: {x,rule_nums} \notin layer_set
temp_one == CHOOSE z \in {{x,y}: x \in 0..10, y \in {-1,rule_nums}}: z \in layer_set
temp_two == CHOOSE z \in {{x,y}: x \in 0..10, y \in {-1,rule_nums}}: z \in (layer_set\{temp_one})
temp == {temp_num,rule_nums}
IN
/\ cur_state = 4
/\ layer_set' = layer_set \union temp
/\ layer_connection_set' = layer_connection_set \union {<<temp_one,temp_two,temp>>}
/\ UNCHANGED << in_seq,cur_state,cur_scope,rule_nums >>
Next == state_changer \/ state_stabler \/ scope_changer \/ derived_def_global \/ rule_head \/ derived_def_rule \/ check_statement
Spec == Init /\ [][Next]_vars
=============================================================================
I check my spec using in_layer_names <- {1,2,3,4} and in_sentence_seq <- <<1,2,3,4,5>>.Both in ordinary assignments.
And my problems are as follows:
1.TLC reports actions derived_def_global,derived_def_rule,check_statement are never enabled.
2.TLC reports error no.1 that my spec is attempting to compare integer 0 with non-integer: {-1, 3}.
3.TLC reports error no.2 occurred when TLC was evaluating the nested expressions in line 75 and 76.
I wonder how to rewrite my spec to make it run as what I think and solve these problems.And I hope my silly descriptions and problems won't bother you and make you angry.(
Thank you.
As per my comment, you may solve some of your problems (and get closer to the system you are trying to model) by replacing CHOOSE with \E. For example, you could rewrite check_statement this way:
check_statement ==
\E temp_num \in 0..10:
/\ {temp_num,rule_nums} \notin layer_set
/\ \E temp_one \in {{x,y}: x \in 0..10, y \in {-1,rule_nums}}:
/\ temp_one \in layer_set
/\ \E temp_two \in ...:
/\ ...
This is a good idea because in TLA+ CHOOSE performs an arbitrary but deterministic choice, and I suspect you actually want to explore every possible choice.