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

Re: [tlaplus] Parser Error



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.