Parser Error

[Sara Zain]

Hi! I just downloaded the TLA toolbox. However,  I am getting this error "Parser error" notification. Can anyone help me, please? Also, I don't see a TLA module and directory path compare to what I see in the video tutorial. 

[Stephan Merz]

Typo “Intergers”

Stephan  

On 28 Apr 2023, at 11:31, Sara Zain <sara...@tu-dresden.de> wrote:

Hi! I just downloaded the TLA toolbox. However,  I am getting this error "Parser error" notification. Can anyone help me, please? Also, I don't see a TLA module and directory path compare to what I see in the video tutorial. 

<Screenshot from 2023-04-28 11-31-09.png>

--
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...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/f247500f-7679-4f68-8d62-920b5f2f945bn%40googlegroups.com.

<Screenshot from 2023-04-28 11-31-09.png>

[hwa...@gmail.com]

Parser really needs to show line numbers :/

H

[Sara Zain]

Hi all,

I am getting this TLC error for the following code. Any idea please?

Thank you.

Regards,

Sara 

_________________________________________________________

EXTENDS
        \*Crypto,
        Integers, FiniteSets, TLC, Sequences

CONSTANTS
    Client, Server, Msg,
    SK_c, SK_s,  \* private keys
    N,         \* nonce
    Certificate,         \* certificate
    Sig      \* signature

VARIABLES
    State,               \* current state
    Current_Msg,         \* current message
    Current_State        \* current state of the secure channel
   
Init ==
    /\ State = "Init"
    /\ Current_State = << SK_c, SK_s, N, Certificate, Sig >>
 
Handshake ==
    /\ State = "Handshake"
    /\ Current_Msg = << "Hello" >>
    /\ Current_State[6] = <<Certificate, Sig>>       \* send certificate and signature
    /\ State' = "Finished"
    /\ UNCHANGED << Current_State, Current_Msg >>
 
 DataTransfer ==
    /\ State = "Finished"
    /\ Current_Msg = << "Data", "Secret message" >>
    (*/\ S[6] = Encrypt(S[2], S[5], M[2], S[6])*) \* encrypt message with server's key
    /\ State' = "Closed"
    /\ UNCHANGED << Current_State, Current_Msg >>
   
 Next == Handshake \/ DataTransfer
 
 InitStates == << Init >>
 NextStates == Next
 
 SecureChannelInvariant ==
    /\ Current_State[1] # Current_State[2] \* private keys are different
    /\ Current_State[3] # N    \* nonce is different each time
    /\ Len(Current_State[4]) > 0  \* certificate is not empty
    /\ Len(Current_State[5]) > 0  \* signature is not empty
    /\ Len(Current_State[6]) > 0  \* IV is not empty
 
 TypeOK ==
    /\ State \in {"Init", "Handshake", "Finished", "Closed"}
    /\ Len(Current_Msg) = 2
    /\ Current_Msg[1] \in {"Hello", "Data"}
   
  SecureChannel ==
    /\ State = "Handshake" => Len(Current_State) = 6
    /\ State = "Finished" => Len(Current_State) = 7
    /\ State = "Closed" => Len(Current_State) = 7
    /\ SecureChannelInvariant

 NextStep == Next /\ TypeOK
 Spec == Init /\ [][NextStep]_<<State, Current_State>>

[Stephan Merz]

Do you have any specific reason to exclude that variable from the subscript?

I also notice that that variable is not constrained by the initial condition and that the typing invariant asserts

Len(Current_Msg) = 2

whereas action Handshake requires it to be of length 1??

Stephan

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/d60e90ec-1339-4d45-9260-4f7cb183028cn%40googlegroups.com.
<Screenshot from 2023-05-08 16-48-43.png>

[Sara Zain]

Hi Stephan,

may I know which variable you are referring to?

thank you!

Regards,

Sara

---------------

Dr. Sara Zain

Postdoctoral Research Associate

Technische Universität Dresden,

Dept. of Computer Science, 

Systems Engineering Group.

Office: APB 3077

Phone: +49 351 463-42358

Website: https://tu-dresden.de/ing/informatik/sya/se/die-professur/beschaeftigte/sara_zain?set_language=en

---

From: tla...@googlegroups.com <tla...@googlegroups.com> on behalf of Stephan Merz <stepha...@gmail.com>
Sent: 08 May 2023 17:10:03
To: tla...@googlegroups.com
Subject: Re: [tlaplus] Parser Error

 

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/C0478BD4-0471-4F7F-8BFB-545A746CDEBA%40gmail.com.

[Stephan Merz]

Variable Current_Msg, which is mentioned in the error message (and which is the only variable that does not appear in the subscript of the next-state relation).

Stephan

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/e51ccec9cb234989a80188b356122b36%40tu-dresden.de.

[Sara Zain]

ahh I see! But now, I have changed the last two lines of code to the following, and I am getting this error now?

 InitNext == Init \in InitStates    (* warning sign: InitNext is never enabled*)
 Spec ==  InitNext /\ [][Next]_<<State,Current_Msg,Current_State>>

Regards,

Sara

[Jones Martins]

Hi Sara,

You had written "InitStates == <<Init>>" and then, "InitNext == Init \in InitStates". Since InitStates is a sequence, and not a set, I don't think that's correct, the formula evaluates to False and InitNext is never enabled (never true). Maybe changing InitStates to a set? (InitStates == { Init })

Jones

[Stephan Merz]

In fact, Init is a predicate (a Boolean expression), so << Init >> is a sequence containing a Boolean. Also, writing

Init \in { Init }

simply evaluates to TRUE and is therefore not helpful. Your original specification

Init /\ [][Next]_vars

(where vars is the tuple of all variables of your specification) is of the right form, assuming that it contains conditions

var = ...    or   var \in ...

for every variable var. TLC will interpret such conditions and use them for constructing the initial states.

Have you actually followed an introduction to TLA+ such as Lamport's video lectures? Did you take the time to play with TLA+ specifications available online before writing your own spec from scratch? Although members of the TLA+ Google group are generally willing to help you with the problems that you encounter, it appears to me that this approach to correcting errors one by one is much less efficient than investing some time in learning how to use the language and its tools.

Stephan

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/fd4f7b70-9b92-4fd2-a15e-d4d94f8c897dn%40googlegroups.com.