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

*From*: Jones Martins <jonesmvc@xxxxxxxxx>*Date*: Mon, 8 May 2023 15:21:19 -0700 (PDT)*References*: <f247500f-7679-4f68-8d62-920b5f2f945bn@googlegroups.com> <BABF7502-A395-446E-A96E-2B17215767A1@gmail.com> <e045407f-998b-487c-a37f-286d7883f1a6n@googlegroups.com> <d60e90ec-1339-4d45-9260-4f7cb183028cn@googlegroups.com> <C0478BD4-0471-4F7F-8BFB-545A746CDEBA@gmail.com> <e51ccec9cb234989a80188b356122b36@tu-dresden.de> <4426543A-87C0-4669-8F13-BA14F4668BDF@gmail.com> <11d676cd-52cf-4c6c-b5da-0c77c0190582n@googlegroups.com>

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,SaraOn 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).StephanOn 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 ZainPostdoctoral Research Associate

Technische Universität Dresden,Dept. of Computer Science,Systems Engineering Group.Office: APB 3077Phone: +49 351 463-42358From:tla...@xxxxxxxxxxxxxxxx <tla...@xxxxxxxxxxxxxxxx> on behalf of Stephan Merz <stepha...@xxxxxxxxx>Sent:08 May 2023 17:10:03To:tla...@xxxxxxxxxxxxxxxxSubject:Re: [tlaplus] Parser ErrorDo 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 assertsLen(Current_Msg) = 2whereas action Handshake requires it to be of length 1??--StephanOn 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>>Parser really needs to show line numbers :/HOn Friday, April 28, 2023 at 4:59:12 AM UTC-5 Stephan Merz wrote:Typo “Intergers”StephanOn 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.To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/e51ccec9cb234989a80188b356122b36%40tu-dresden.de.

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.

**Follow-Ups**:**Re: [tlaplus] Parser Error***From:*Stephan Merz

**References**:**[tlaplus] Parser Error***From:*Sara Zain

**Re: [tlaplus] Parser Error***From:*Stephan Merz

**Re: [tlaplus] Parser Error***From:*hwa...@xxxxxxxxx

**Re: [tlaplus] Parser Error***From:*Sara Zain

**Re: [tlaplus] Parser Error***From:*Stephan Merz

**Re: [tlaplus] Parser Error***From:*Sara Zain

**Re: [tlaplus] Parser Error***From:*Stephan Merz

**Re: [tlaplus] Parser Error***From:*Sara Zain

- Prev by Date:
**[tlaplus] Collision probability of TLC state computation** - Next by Date:
**[tlaplus] Liveness only when a certain condition holds** - Previous by thread:
**Re: [tlaplus] Parser Error** - Next by thread:
**Re: [tlaplus] Parser Error** - Index(es):