I'm now writing a spec which needs a 2D array and a stack,
and I need to assign the 2D array with some values in initial state,
also give this 2D array a range of possible values in typeinvariant,
like a function.
So I write some part of my spec like this because I don't know how to assign 2D array in initial state ,in which variable predict_table is the 2D array :
TypeInvariant == /\ stack \in Seq(all_syntax_symbol)
/\ token_pointer \in 1..Len(input_token)+1
/\ predict_table \in [ grammar_symbol_set -> [ terminal_symbol_set -> Seq(all_syntax_symbol)]]
/\ parsing_status \in 0..3
Init == /\ stack = <<13,-1>>
/\ token_pointer = 1
/\ predict_table = [x \in grammar_symbol_set,y \in terminal_symbol_set |-> <<>>]
/\ parsing_status = 0
Action_1 == /\ parsing_status = 0
/\ parsing_status' = 1
/\ predict_table' = [predict_table EXCEPT ![-1][12] = <<-9,-3,-2>>,![-2][12] = <<11,4,12>>,![-3][4]= <<-4,10,4>>,![-4][7]= <<-7>>,![-4][8]= <<-6>>,![-4][9]= <<-5>>,![-5][9]= <<-8,-8,9>>,![-6][8]= <<-8,-8,8>>,![-7][7]= <<-8,-8,7>>,![-8][4]= <<4>>,![-8][6]= <<5,-4,6>>,![-9][3]= <<1,-10,-3,2,3>>,![-10][7]= <<-7>>,![-10][8]= <<-6>>,![-10][9]= <<-5>>]
/\ UNCHANGED <<stack,token_pointer>>
However TLC told me that the way I assign in init(and maybe in Action_1?) and make it invariant in TypeInvariant is not OK.
And I don't know how to make it correct.
Another question is about push and pop action of stack in my spec.
I write them in this way,in which variable stack just mean my FILO stack:
Action_2 == /\ parsing_status = 1
/\ (stack[Len(stack)] = input_token[token_pointer]) /\ (stack[Len(stack)] \in terminal_symbol_set)
/\ stack' = IF Len(stack)>1 THEN SubSeq(stack,1,Len(stack)-1) ELSE <<>>
/\ parsing_status' = IF Len(stack) = 1 THEN 3 ELSE 1
/\ token_pointer' = token_pointer+1
/\ UNCHANGED <<predict_table>>
Action_5 == /\ parsing_status = 1
/\ (predict_table[stack[Len(stack)]][input_token[token_pointer]] # <<>>) /\ (predict_table[stack[Len(stack)]][input_token[token_pointer]] # <<0>>)
/\ stack' = IF Len(stack)>1 THEN SubSeq(stack,1,Len(stack)-1) \o predict_table[stack[Len(stack)]][input_token[token_pointer]] ELSE predict_table[stack[Len(stack)]][input_token[token_pointer]]
/\ UNCHANGED <<parsing_status,token_pointer,predict_table>>
I wonder whether the pop action in Action_2 and push action in Action_5 of my stack is good in functionality.
And here is my full spec,
imitating the predictive parsing algorithm,
while the grammar making up the predict table is in LL(1).
I wonder if there're more syntax errors in it
, and it'd be grateful if you could tell me:
----------------------------- MODULE Parser_DFA -----------------------------
EXTENDS Integers,Naturals,Reals,Sequences
CONSTANTS input_token
VARIABLES stack,token_pointer,predict_table,parsing_status
vars == <<stack,token_pointer,predict_table,parsing_status>>
grammar_symbol_set == -10..-1
\* non-terminal symbol set
terminal_symbol_set == 1..13
\* terminal symbol set, 13 stands for EOF($)
all_syntax_symbol == grammar_symbol_set \union terminal_symbol_set \union {0}
\* 0 stands for epslion(
ε
)
TypeInvariant == /\ stack \in Seq(all_syntax_symbol)
/\ token_pointer \in 1..Len(input_token)+1
/\ predict_table \in [ grammar_symbol_set -> [ terminal_symbol_set -> Seq(all_syntax_symbol)]]
/\ parsing_status \in 0..3
Init == /\ stack = <<13,-1>>
/\ token_pointer = 1
/\ predict_table = [x \in grammar_symbol_set,y \in terminal_symbol_set |-> <<>>]
/\ parsing_status = 0
\*init state of predictive parsing
Action_1 == /\ parsing_status = 0
/\ parsing_status' = 1
/\ predict_table' = [predict_table EXCEPT ![-1][12] = <<-9,-3,-2>>,![-2][12] = <<11,4,12>>,![-3][4]= <<-4,10,4>>,![-4][7]= <<-7>>,![-4][8]= <<-6>>,![-4][9]= <<-5>>,![-5][9]= <<-8,-8,9>>,![-6][8]= <<-8,-8,8>>,![-7][7]= <<-8,-8,7>>,![-8][4]= <<4>>,![-8][6]= <<5,-4,6>>,![-9][3]= <<1,-10,-3,2,3>>,![-10][7]= <<-7>>,![-10][8]= <<-6>>,![-10][9]= <<-5>>]
/\ UNCHANGED <<stack,token_pointer>>
\*still init state of predictive parsing,but for predictive table assignment.
Action_2 == /\ parsing_status = 1
/\ (stack[Len(stack)] = input_token[token_pointer]) /\ (stack[Len(stack)] \in terminal_symbol_set)
/\ stack' = IF Len(stack)>1 THEN SubSeq(stack,1,Len(stack)-1) ELSE <<>>
/\ parsing_status' = IF Len(stack) = 1 THEN 3 ELSE 1
/\ token_pointer' = token_pointer+1
/\ UNCHANGED <<predict_table>>
\* detects a terminal symbol and matchs in input_token and stack,pop and pointer++
\* parsing_status =1 means OK, 2 means error, 3 means finished without error
Action_2_null == /\ parsing_status = 1
/\ predict_table[stack[Len(stack)]][input_token[token_pointer]] = <<0>>
/\ stack' = IF Len(stack)>1 THEN SubSeq(stack,1,Len(stack)-1) ELSE <<>>
/\ parsing_status' = IF Len(stack) = 1 THEN 3 ELSE 1
/\ UNCHANGED <<parsing_status,predict_table>>
\* detects a epslion(
ε
) in predictive table, just pop in stack is OK
Action_3 == /\ parsing_status = 1
/\ stack[Len(stack)] \in terminal_symbol_set
/\ stack[Len(stack)] # input_token[token_pointer]
/\ parsing_status' = 2
/\ UNCHANGED <<stack,token_pointer,predict_table>>
\* detects a terminal symbol and not match in input_token and stack, means error.
Action_4 == /\ parsing_status = 1
/\ predict_table[stack[Len(stack)]][input_token[token_pointer]] = <<>>
/\ parsing_status' = 2
/\ UNCHANGED <<stack,token_pointer,predict_table>>
\* parsing error(predictive table of this pair of symbol is empty)
Action_5 == /\ parsing_status = 1
/\ (predict_table[stack[Len(stack)]][input_token[token_pointer]] # <<>>) /\ (predict_table[stack[Len(stack)]][input_token[token_pointer]] # <<0>>)
/\ stack' = IF Len(stack)>1 THEN SubSeq(stack,1,Len(stack)-1) \o predict_table[stack[Len(stack)]][input_token[token_pointer]] ELSE predict_table[stack[Len(stack)]][input_token[token_pointer]]
/\ UNCHANGED <<parsing_status,token_pointer,predict_table>>
\* detects a non-terminal symbol and update the stack.
Next == Action_1 \/ Action_2 \/ Action_2_null \/ Action_3 \/ Action_4 \/ Action_5
Spec == Init /\ [][Next]_vars
Invariant_1 == parsing_status = 3 => token_pointer = Len(input_token)
\*means parsing finished
Invariant_2 == parsing_status = 2 => Len(stack) # 0
\*means parsing error and not finished
=============================================================================
Thank you for your reading.
I know it's quite long but this's the best I can describe my question.
I'm sorry for that.