[
https://issues.apache.org/jira/browse/CASSANDRA-18682?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=17748625#comment-17748625
]
Henrik Ingo edited comment on CASSANDRA-18682 at 7/28/23 2:11 PM:
------------------------------------------------------------------
Weekly status update:
* Decided to get rid of PlusCal. It's easy, the PlusCal code is compiled into
TLA+, so just remove the PlusCal and you're left with the equivalent TLA+
implementation.
* TLA Toolbox still feels it's on shaky ground. Decided to try
[PlusPy|https://github.com/tlaplus/PlusPy], a Python implementation of the TLA+
syntax. One motivation here is that by reading the Python code, it could be
easier to at least understand what it is trying to do. In the extreme case one
could make careful modifications to avoid some of the oddest TLA+ syntax...
* However, PlusPy quite early on raises an exception on me. After two days I
found out what was wrong (variables need to be initialized). Patch below. After
fixing that issue, there's now an exception because it doesn't find the Init
stage... In summary, this could work, but how confident would we be that it is
checking anything correctly at all, if I have to supply N fixes to even run the
thing.
* Took a step back and decided to read up on alternatives to TLA+. Through
[Wikipedia|https://en.wikipedia.org/wiki/List_of_model_checking_tools], found
[Mazzanti, Franco; Ferrari, Alessio (2018)|https://arxiv.org/abs/1803.10324v1]
who implemented the same algorithm in 10 different tools and share their
results. [They later have produced a 100+ page report surveying what tools are
used the
most.|http://www.astrail.eu/download.aspx?id=bb46b81b-a5bf-4036-9018-cc6e7d91e2c2]
TLA+ isn't one of them...
* Based on that report, I'm curious now to test the [Eclipse based Rodin
framework,|http://www.event-b.org/] and the Event-B language it uses. That's
for next week.
{{diff --git a/pluspy.py b/pluspy.py}}
{{index d1ba07a..2103fcf 100644}}
{{--- a/pluspy.py}}
{{+++ b/pluspy.py}}
{{@@ -2185,7 +2185,10 @@ class VariableExpression(Expression):}}
{{ if initializing:}}
{{ return PrimeExpression(expr=subs[self])}}
{{ else:}}
{{- return subs[self]}}
{{+ v = subs[self]}}
{{+ if isinstance(v,bool):}}
{{+ v = ValueExpression(v)}}
{{+ return v}}
{{ }}
{{ def eval(self, containers, boundedvars):}}
{{ print("Error: variable", self.id, "not realized", containers,
boundedvars)}}
was (Author: henrik.ingo):
Weekly status update:
* Decided to get rid of PlusCal. It's easy, the PlusCal code is compiled into
TLA+, so just remove the PlusCal and you're left with the equivalent TLA+
implementation.
* TLA Toolbox still feels it's on shaky ground. Decided to try
[PlusPy|https://github.com/tlaplus/PlusPy], a Python implementation of the TLA+
syntax. One motivation here is that by reading the Python code, it could be
easier to at least understand what it is trying to do. In the extreme case one
could make careful modifications to avoid some of the oddest TLA+ syntax...
* However, PlusPy quite early on raises an exception on me. After two days I
found out what was wrong (variables need to be initialized). Patch below. After
fixing that issue, there's now an exception because it doesn't find the Init
stage... In summary, this could work, but how confident would we be that it is
checking anything correctly at all, if I have to supply N fixes to even run the
thing.
* Took a step back and decided to read up on alternatives to TLA+. Through
[Wikipedia|https://en.wikipedia.org/wiki/List_of_model_checking_tools], found
[Mazzanti, Franco; Ferrari, Alessio (2018)|https://arxiv.org/abs/1803.10324v1]
who implemented the same algorithm in 10 different tools and share their
results. [They later have produced a 100+ page report surveying what tools are
used the
most.|http://www.astrail.eu/download.aspx?id=bb46b81b-a5bf-4036-9018-cc6e7d91e2c2]
TLA+ isn't one of them...
* Based on that report, I'm curious now to test the [Eclipse based Rodin
framework,|http://www.event-b.org/] and the Event-B language it uses. That's
for next week.
> Create TLA+ spec of Accord
> --------------------------
>
> Key: CASSANDRA-18682
> URL: https://issues.apache.org/jira/browse/CASSANDRA-18682
> Project: Cassandra
> Issue Type: Task
> Components: Accord
> Reporter: Henrik Ingo
> Assignee: Henrik Ingo
> Priority: Normal
> Fix For: 5.x
>
>
> Create a TLA+ Spec of Accord.
>
> For this ticket, goal is just to cover Algorithm 1. No significant
> discoveries are expected, and to really check correctness, one will have to
> implement all 4 algorithms.
--
This message was sent by Atlassian Jira
(v8.20.10#820010)
---------------------------------------------------------------------
To unsubscribe, e-mail: commits-unsubscr...@cassandra.apache.org
For additional commands, e-mail: commits-h...@cassandra.apache.org
