[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Some questions about writing 2D array with assignment and stack



Thank you very much,I'll try it now. :)

在2023年1月13日星期五 UTC+8 21:55:19<Stephan Merz> 写道:
The two sets of functions [A -> [B -> S]] and [A \X B -> S] are not the same, although they are isomorphic.

Either change your corresponding conjunct in TypeInvariant to

  predict_table \in [grammar_symbol_set \X terminal_symbol_set -> Seq(all_syntax_symbol)]

or change your initialization to

  predict_table = [x \in grammar_symbol_set |-> [y \in terminal_symbol_set |-> <<>>]]

– whichever is more convenient to use in the rest of the spec. If you go down the first route, you want to change your update in Action 1 to

  predict_table' = [predict_table EXCEPT ![-1,12] = <<-9,-3,-2>>, ...]

For the stack operations, some of the definitions in the SequencesExt module [1] from the Community Modules may come in handy.

Stephan

[1] https://github.com/tlaplus/CommunityModules/blob/master/modules/SequencesExt.tla


On 13 Jan 2023, at 14:41, Delta Striker <unicorn8...@xxxxxxxxx> wrote:

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.

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/0f8dd7c1-d524-4030-880f-a1c8b7f71acdn%40googlegroups.com.

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/9346ad4f-734c-43c9-9e0d-1e1af6093a67n%40googlegroups.com.