Hi. I was upgrading to the latest version and noticed that new trait bounds were introduced (e.g. Ord for Actor::Message). If I understand correctly, this prevents the use of e.g. HashMap's in such messages. Would it be possible to relax these trait bounds?

(I tried to perform such change, but it turned out more complex than what I was expecting (probably because I'm not familiar with the codebase). If you have ideas on how to go about this, I can give it a try. Thanks.)

This PR adds permutation based symmetry checking.

It currently works by checking whether there are any permutations of the current state, who's fingerprint is within generated and in that case not persuing that state further.

This is not an efficient approach for doing symmetry checking, but for low numbers of symmetric elements, this can improve the model checking time. For an example of this test the increment_lock.rs example (which models multiple threads trying to increment a variable), goes from 38169180 states to 41 states. Unfortunately this takes longer to check since it fingerprints 10! states per actual state.

Additionally the actual interface for this feature is not very user friendly, requiring the user to manually implement a permutation function. This may be possible to fix using hash maps.

A more efficient approach would be to canonicalise each state before fingerprinting (sort hashmaps etc by non-symmetric elements) such that two symmetric states should end up having the same hash in most cases.

TODO

• [ ] add tests
• [ ] optimise

I recently tried to write the Ballot Leader Election with Gossiping using Stateright and encountered some issues along the way.

I can not stop Stateright from generating new states. Even though I added a maximum of rounds to stop the set-up of the timer, it keeps generating states.

Are there issues with using the function on_timeout?

Repo: https://github.com/Nightcro/ble-stateright

Hello! Love this project. I had a thought the other day...Futures are state machines, and stateright explores state space. Rather than having to manually hoist state into the State associated type forActors, would it possible to automatically plug stateright into the generated state machine for futures? Essentially treating futures as actors, where the state is always Poll::Ready(val) or Poll::Pending?

This is a note about an addition I'm thinking of making -- thought I'd post here before I work on it to ask if it makes sense to you and/or would be welcome.

(Context: the actor system I'm driving with stateright exhibits pretty bad state-space explosion -- 3 peers and 2 consensus cycles finish in "only" a few hundred thousand states, but 3 consensus cycles exceeds 100m states and exhausts memory on my 128gb test box -- so I'm kinda grasping at straws to figure out things to reduce it, and/or whether there's a bug in my code. I'll file a couple other issues as possible avenues I'm considering for discussion of those also.)

The simplest change I can think of is to add another flag concerning the network semantics, such that messages in a given flow don't get reordered: if peer 1 sends messages A then B to peer 2, I'd like to only explore delivery schedules that have A arriving at peer 2 before B. I think this is not an unreasonable variant -- lots of network abstractions preserve order per-flow -- and it'll cut out a lot of the state space, for a reasonably small change.

This would not alter the interleaving of separate flows: if peer 3 sends message C to peer 2, then we'd still explore arrival schedules at peer 2 of each of [C,A,B], [A,C,B], [A,B,C]. Just not [C,B,A], [B,C,A], or [B,A,C].

What do you think?

• Adds properties field per-state in the explorer API
• Renders property icons per-state (toggleable)
• Renders properties for currently selected state (toggleable)
• Renders breadcrumbs for states on a path to a discovery

Fixes #22

When exploring states in the UI it shows the overall properties for all states so far, could it also show the status of the properties at the current state being explored.

My hope is that this will allow us to automatically be told (when clicking through) that we are now in a bad state (violating properties).

This PR adds a simple form of liveness-proerty checking -- "eventually" properties. They're implemented by assigning a bit-number to each such property and propagating a compact bitset (IdSet from the id-set crate) representing properties not-yet-established on a given path, along with the state, in the queue of states. Any property still not-yet-established when we arrive at a terminal state is marked as a counterexample discovery, as with "always" properties, and reported the same way.

These properties suffer from two possible false negatives:

• Cyclic paths are not disambiguated from DAG joins, so neither is considered terminal. If an eventually property is not met by the cycle-closing edge of a cyclic path, it is forgotten.
• DAG joins with different sets of liveness properties at the join point are not differentiated. If an eventually property was met on the first visit through a state but not on the second visit that joins it, it is not reported.

In theory both of these could be converted to a false positive by considering revisited states as terminal. I'd be open to the argument that that's more-useful / more-correct. Not sure what's more annoying to users in practice; the code is anyways factored in such a way that you'd only have to add one more call to note_terminal_state to switch to that way, if you prefer.

Hi! Thanks so much for building this library, it's great!

As a first contribution, here's a change that lets users prune the portion of search space that consists of duplicate messages -- some systems have trivially idempotent messages, where exploring all the extra delivery schedules is just a waste of model-checking time.

This checker waits for requests to check fingerprints before doing the checking. This makes exploring less resource-intensive, without the need to check every state to just explore a few paths.

There is a 'run to completion' button in the UI for letting the checker run without waiting, back to the normal functionality.

The checker itself is mostly a copy of the BFS checker, besides the modifications to wait for fingerprints.

A potential future change would be to merge this control-flow functionality into both the DFS and BFS checkers directly

The -i lo0 parameter referrers to the device/interface that tcpdump will listen on and not all systems use lo0 to refer to the loop back interface. Executing tcpdump -D will display a list of devices available on the system and the user can find the current loop back device:

For instance on my computer device 3, lo, is the loop back device:

$ tcpdump -D 1.wlp170s0 [Up, Running, Wireless, Associated] 2.any (Pseudo-device that captures on all interfaces) [Up, Running] 3.lo [Up, Running, Loopback] 4.bluetooth0 (Bluetooth adapter number 0) [Wireless, Association status unknown] 5.bluetooth-monitor (Bluetooth Linux Monitor) [Wireless] 6.nflog (Linux netfilter log (NFLOG) interface) [none] 7.nfqueue (Linux netfilter queue (NFQUEUE) interface) [none] 8.dbus-system (D-Bus system bus) [none] 9.dbus-session (D-Bus session bus) [none]

Hello author, I am very interested in the stateright project, especially its model checker, and I have also tried it. I personally think that Rust is easier to use than TLA+ in terms of writing specifications. However, most of our project teams are familiar with Go and Java code, so we would like to try to use the Go language to implement the stateright project to facilitate its promotion and use. Could you please provide the structure flow chart of the Stateright project, or other information related to Stateright, so as to facilitate our development. If you are interested, we especially welcome you to join to develop the go version of stateright to make it more valuable. thank you!

It would be really nice to be able to have the results of a check be saved (including states created/visited etc) so that they could be shared without others having to rerun the check.

Maybe this could lead to the web explorer having an option to upload a file with the check that it can process into an explorable version.

I guess this wouldn't directly mean that the checker can continue from a persisted state but could also enable snapshots while checking is running to enable investigating issues later.

In stateright, is it possible for the "environment" to have state? Or is all of the state represented in the actors?

For example, could the environment have a clock that is non-deterministically updated?

(Sorry for the naive question.)

A fair number of explicit-state model checkers use DFS not BFS. I realize this would be a fairly big revision to the structure (at least of the checker module) but I think there are good reasons for it:

• We can spit the sources (visited-state-tracking) hashtable in two: one piece that's a strictly-consulted and unbounded (but probably quite small), containing the current DFS path, used for detecting re-visits on a single path; and a second piece that's a size-bounded (randomly evicting on overflow) set of previously-visited states not on the current DFS path. A false negative on the second piece (due to an eviction) causes accidental revisiting of a subspace of the state-space but doesn't affect termination of the algorithm. This allows trading time and space: specifically avoiding memory exhaustion, at the cost of a longer runtime.
• I think it might better-enable distributed operation in the future (on a cluster of machines) by delegating entire subtrees to separate nodes. Not sure about this.
• More significantly, I think it's a path towards doing dynamic partial-order reduction (as described here: https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.421.1291). Specifically in an actor system we could classify the choice-points in a given DFS path as splitting or not-splitting the future state space into disjoint sets of communicating actors and only backtrack and reorder within a given disjoint set.

I'm not sure about drawbacks. Maybe a slightly more complicated stack-of-choice-points structure to track progress? What do you think?

Currently it looks like the checker always splits chunks off the end of the pending vecdeque, and then pushes new extensions back on the end. But it doesn't necessarily split off everything pending, and it can often grow the end by more than it tried to consume. When this happens, it ignores (potentially for a very long time, until much later in the run) entries earlier in the deque.

I'm not sure this is a problem (I guess if we're going to explore all states eventually the order might not matter?) but I worry a bit vaguely that there's some possibility that an imbalance in the shape the frontier gets expanded at will wind up costing more work or more memory than if it were more balanced.

Might it make sense to randomize or otherwise permute the pending vector from time to time?