On 18 Dec 2022, at 13:24, Deividas Bražėnas <deividas...@trafi.com> 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>>
2. I want to specify global variable bcValue in Init based on the set of bcNode/\ \/ bcNode \in CN /\ bcValue \in Value\/ bcNode \in FN /\ bcValue = NotValue
<<"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"]} )>>
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...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/3fb78eb2-9d83-4e1b-b747-29a683469f7an%40googlegroups.com.
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...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/0BB14F11-2274-45EF-9121-7CBE50F61AA1%40gmail.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/7763e691-1bdd-4326-a748-e54194e5a189n%40googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/c02fcd12-1f74-4a15-a78c-bee89f45c968n%40googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/9ceea054-2c8a-4dda-8af4-46d5927b6996n%40googlegroups.com.