search

freespek / ssf-mc

EF project Exploring Automatic Model-Checking of the Ethereum specification
Apache License 2.0
4 stars 0 forks source link

Introduce a state machine to generate examples of a single node #8

Closed konnov closed 3 months ago

konnov commented 3 months ago

Basically, we need a TLA+ spec that stores the state of a single node. We simply initialize this spec with Init, and Next keeps things UNCHANGED. The whole point of this spec is to experiment with the definitions.