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

Re: [tlaplus] Parser Error

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


On 9 May 2023, at 00:21, Jones Martins <jonesmvc@xxxxxxxxx> wrote:

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
On Monday, 8 May 2023 at 12:47:28 UTC-3 Sara Zain wrote:
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

Screenshot from 2023-05-08 17-43-05.png


On Monday, May 8, 2023 at 5:26:44 PM UTC+2 Stephan Merz wrote:
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

On 8 May 2023, at 17:24, Sara Zain <sara...@xxxxxxxxxxxxx> wrote:

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
From: tla...@xxxxxxxxxxxxxxxx <tla...@xxxxxxxxxxxxxxxx> on behalf of Stephan Merz <stepha...@xxxxxxxxx>
Sent: 08 May 2023 17:10:03
To: tla...@xxxxxxxxxxxxxxxx
Subject: Re: [tlaplus] Parser Error
 
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

On 8 May 2023, at 16:52, Sara Zain <sara...@xxxxxxxxxxxxx> wrote:

<Screenshot from 2023-05-08 16-48-43.png>
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>>


On Monday, May 1, 2023 at 8:38:27 PM UTC+2 hwa...@gmail.com wrote:
Parser really needs to show line numbers :/

H

On Friday, April 28, 2023 at 4:59:12 AM UTC-5 Stephan Merz wrote:
Typo “Intergers”

Stephan  


On 28 Apr 2023, at 11:31, Sara Zain <sara...@xxxxxxxxxxxxx> 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...@xxxxxxxxxxxxxxxx.
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>

-- 
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/d60e90ec-1339-4d45-9260-4f7cb183028cn%40googlegroups.com.
<Screenshot from 2023-05-08 16-48-43.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...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/C0478BD4-0471-4F7F-8BFB-545A746CDEBA%40gmail.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+u...@xxxxxxxxxxxxxxxx.

-- 
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/fd4f7b70-9b92-4fd2-a15e-d4d94f8c897dn%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/4181E31D-2B41-4AF1-A4CA-D6A567A6F1A3%40gmail.com.