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

*From*: Deividas Bražėnas <deividas.brazenas@xxxxxxxxx>*Date*: Wed, 21 Dec 2022 13:07:06 -0800 (PST)*References*: <d5726e3d-1761-4bac-be66-dbb788f7b42cn@googlegroups.com> <EF2E36DD-EB82-4CF4-9383-34E258045780@gmail.com> <3fb78eb2-9d83-4e1b-b747-29a683469f7an@googlegroups.com> <D2B7A8E7-AE47-41CB-8696-1E4378B8E348@gmail.com> <1b6b78c3-0887-4e54-8490-f55f500b3b04n@googlegroups.com> <0BB14F11-2274-45EF-9121-7CBE50F61AA1@gmail.com> <CAMVPFU8DveO_EYrKkAOjtOTRTTbHSPUw75LUUJ9Q5snfA02ppg@mail.gmail.com> <7763e691-1bdd-4326-a748-e54194e5a189n@googlegroups.com> <D69C600E-6CB4-439C-BD6D-46168951F07E@gmail.com> <c02fcd12-1f74-4a15-a78c-bee89f45c968n@googlegroups.com> <BF97F189-B53C-45D6-A2B4-B79313DCAF6C@gmail.com>

Hey Stephan,

I'm a bit confused after your previous answer - what would be the correct way to write that **with **statement in my case?

Sorry if that is a dumb question 🤦♂️.

Deividas

On Wednesday, December 21, 2022 at 2:34:54 PM UTC+2 Stephan Merz wrote:

Within a form [f EXCEPT ![x] = g(@)] (to which a PlusCal assignment f[x] := ... translates), `@' designates f[x]. `@' has no meaning in the right-hand side of an _expression_ [x \in S |-> ...], sorry for the syntax error.StephanOn 21 Dec 2022, at 12:58, Deividas Bražėnas <deividas...@xxxxxxxxx> wrote:Sorry, that was my typo, PlusCal translation seems to be alright.Talking about your proposed solution, what does "@" means here? I get the following error during TLC "@ used where its meaning is not defined."DeividasOn Wednesday, December 21, 2022 at 10:46:15 AM UTC+2 Stephan Merz wrote:The two commas look wrong: this could be an error in the PlusCal translator. If you can confirm this, could you open a GitHub issue? Could you share the entire TLA+ module?What happens if you write something likewith m = [t |-> "PROPOSE", v |-> input] domsgs := [p \in peers |-> @ \cup {m}]end withStephanOn 21 Dec 2022, at 09:40, Deividas Bražėnas <deividas...@xxxxxxxxx> wrote:I'm also wondering, maybe it would be possible to do that in a more simpler way? e.g. something like this:msgs := [peer_id \in peers |-> msgs[peer_id] \cup {[t |-> "PROPOSE", v |-> input]}];But this one gives me a syntax error at first "|->" operator when generated to following TLA+:msgs' = [peer_id[self] \in peers[self] |-> msgs[peer_id[self]] \cup {[t |-> "PROPOSE", , v |-> input[self]]}]On Wednesday, December 21, 2022 at 10:37:01 AM UTC+2 Deividas Bražėnas wrote:Thanks for the answer, Stephan!On Wed, Dec 21, 2022 at 10:32 AM Stephan Merz <stepha...@xxxxxxxxx> wrote:You can rewrite your loop as follows:while peers # {} dowith p \in peers domsgs[p] := @ \union {...};peers := peers \ {p};end do;end whileNote that unlike your version, this loop iterates through peers in a non-deterministic order, and that this will generate more states when you use TLC for model checking.StephanOn 21 Dec 2022, at 08:59, Deividas Bražėnas <deividas...@xxxxxxxxx> wrote:Hey Stephan, thanks for the clarification and answer.Sorry for not explaining correctly, but I want to simulate the messages sent for peers. So basically, in the end the variable msgs should look like thismsgs = [n_1 |-> {[t |-> "PROPOSE", v |-> "v_1], [t |-> "ECHO", v |-> "v_1]},n_2 |-> {[t |-> "PROPOSE", v |-> "v_1], [t |-> "ECHO", v |-> "v_1]},n_2 |-> {[t |-> "PROPOSE", v |-> "v_1], [t |-> "ECHO", v |-> "v_1]}]And there will be a several processes like SendPropose or SendEcho that would append to set of messages. So sadly your proposed solution will not work :/I've made loop like this work, but I'm wondering whether it would be possible to make it look more prettywhile index <= Len(SetToSeq(peers)) dopeer_id := peers[index];msgs[peer_id] := msgs[peer_id] \union {[t |-> "PROPOSE", v |-> input]};index := index + 1;end while;DeividasOn Wednesday, December 21, 2022 at 9:38:07 AM UTC+2 Stephan Merz wrote:In PlusCal, "with x \in S do ..." expresses non-deterministic choice, not a loop. The body of the "with" instruction is executed for some peer, then TLC backtracks and explores the remaining choices. Remember that TLC is a model checker that explores all runs of an algorithm, not an interpreter that generates one run. Therefore, "print" instructions are often hard to interpret.I am not sure what exactly you are trying to achieve. The end result can of course be obtained by writingmsgs := [pid \in peers |-> [t |-> "PROPOSE"]]StephanOn 20 Dec 2022, at 22:13, Deividas Bražėnas <deividas...@xxxxxxxxx> wrote:Thank you, Stephan!!I'm also wondering how I could write the following in PlusCal.I have these global variables:peers = {n_1, n_2, n_3, n_4}msgs = [node_id \in peers |-> {}]I want to add [t |-> "PROPOSE"] message for every peer in a process.I've tried to do it like this, but it does not work as expected. What may I be doing wrong?print <<"with">>;with peer_id \in peers doprint <<"peers", peers, "peer", peer_id>>;msgs[peer_id] := msgs[peer_id] \union {[t |-> "PROPOSE"]};end with;print <<"msgs", msgs>>;I get the following output:<<"with">>

<<"peers", {n_1, n_2, n_3, n_4}, "peer", n_1>>

<<"msgs", (n_1 :> {[t |-> "PROPOSE"]} @@ n_2 :> {} @@ n_3 :> {} @@ n_4 :> {})>>

<<"peers", {n_1, n_2, n_3, n_4}, "peer", n_2>>

<<"msgs", (n_1 :> {} @@ n_2 :> {[t |-> "PROPOSE"]} @@ n_3 :> {} @@ n_4 :> {})>>

<<"peers", {n_1, n_2, n_3, n_4}, "peer", n_3>>

<<"msgs", (n_1 :> {} @@ n_2 :> {} @@ n_3 :> {[t |-> "PROPOSE"]} @@ n_4 :> {})>>

<<"peers", {n_1, n_2, n_3, n_4}, "peer", n_4>>

<<"msgs", (n_1 :> {} @@ n_2 :> {} @@ n_3 :> {} @@ n_4 :> {[t |-> "PROPOSE"]})>>

Where I would expect:

<<"with">>

<<"peers", {n_1, n_2, n_3, n_4}, "peer", n_1>>

<<"peers", {n_1, n_2, n_3, n_4}, "peer", n_2>>

<<"peers", {n_1, n_2, n_3, n_4}, "peer", n_3>>

<<"peers", {n_1, n_2, n_3, n_4}, "peer", n_4>>

<<"msgs", (n_1 :> {[t |-> "PROPOSE"]} @@ n_2 :> {[t |-> "PROPOSE"]} @@ n_3 :> {[t |-> "PROPOSE"]} @@ n_4 :> {[t |-> "PROPOSE"]} )>>

On Monday, December 19, 2022 at 8:30:20 AM UTC+2 Stephan Merz wrote:Hello,TLA+ is more general than PlusCal, and a systematic conversion to PlusCal is unlikely to yield idiomatic results, if it is possible at all: you will probably end up with a single while loop containing all possible actions. It is a bit like the normal form theorem in computability theory.On 18 Dec 2022, at 13:24, Deividas Bražėnas <deividas...@xxxxxxxxx> wrote:Hello all,I have a TLA+ spec that I'd like to convert to PlusCal, but I'm facing some issues as I don't know how to convert a few parts of the specification.1. I want to have this predicate as a process, but I'm not sure how to convert this part "\E n \in CN, p \in BOOLEAN :"UpdatePredicate ==\E n \in CN, p \in BOOLEAN :/\ predicate[n] => p \* Only monotonic updates are make the algorithm to terminate./\ predicate' = [predicate EXCEPT ![n] = p]/\ UNCHANGED <<bcNode, bcValue, output, msgs>>In PlusCal you could represent this aswith (n \in CN, p \in BOOLEAN) {await (predicate[n] => p);predicate[n] := p}2. I want to specify global variablebcValueinInitbased on the set ofbcNode/\ \/ bcNode \in CN /\ bcValue \in Value\/ bcNode \in FN /\ bcValue = NotValueYou could perhaps writevariablesbcNode \in CN \union FN,bcValue \in (CASE bcNode \in CN -> Value [] bcNode \in FN -> {NotValue});StephanThe content of this email, including all attachments, is confidential. If you are not the intended recipient, please notify us immediately and delete this email. Any disclosure, copying, distribution or any other use of its content is strictly prohibited.--

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/3fb78eb2-9d83-4e1b-b747-29a683469f7an%40googlegroups.com.

The content of this email, including all attachments, is confidential. If you are not the intended recipient, please notify us immediately and delete this email. Any disclosure, copying, distribution or any other use of its content is strictly prohibited.--

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/1b6b78c3-0887-4e54-8490-f55f500b3b04n%40googlegroups.com.

--You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.

To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/9Qe7gvU1rqI/unsubscribe.

To unsubscribe from this group and all its topics, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/0BB14F11-2274-45EF-9121-7CBE50F61AA1%40gmail.com.

The content of this email, including all attachments, is confidential. If you are not the intended recipient, please notify us immediately and delete this email. Any disclosure, copying, distribution or any other use of its content is strictly prohibited.

--

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/7763e691-1bdd-4326-a748-e54194e5a189n%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+u...@xxxxxxxxxxxxxxxx.To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/c02fcd12-1f74-4a15-a78c-bee89f45c968n%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/9ceea054-2c8a-4dda-8af4-46d5927b6996n%40googlegroups.com.

**Follow-Ups**:**Re: [tlaplus] Converting TLA+ spec to PlusCal***From:*Stephan Merz

**References**:**[tlaplus] Converting TLA+ spec to PlusCal***From:*Deividas Bražėnas

**Re: [tlaplus] Converting TLA+ spec to PlusCal***From:*Stephan Merz

**Re: [tlaplus] Converting TLA+ spec to PlusCal***From:*Deividas Bražėnas

**Re: [tlaplus] Converting TLA+ spec to PlusCal***From:*Stephan Merz

**Re: [tlaplus] Converting TLA+ spec to PlusCal***From:*Deividas Bražėnas

**Re: [tlaplus] Converting TLA+ spec to PlusCal***From:*Stephan Merz

**Re: [tlaplus] Converting TLA+ spec to PlusCal***From:*Deividas Bražėnas

**Re: [tlaplus] Converting TLA+ spec to PlusCal***From:*Deividas Bražėnas

**Re: [tlaplus] Converting TLA+ spec to PlusCal***From:*Stephan Merz

**Re: [tlaplus] Converting TLA+ spec to PlusCal***From:*Deividas Bražėnas

**Re: [tlaplus] Converting TLA+ spec to PlusCal***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] Converting TLA+ spec to PlusCal** - Next by Date:
**Re: [tlaplus] Converting TLA+ spec to PlusCal** - Previous by thread:
**Re: [tlaplus] Converting TLA+ spec to PlusCal** - Next by thread:
**Re: [tlaplus] Converting TLA+ spec to PlusCal** - Index(es):