And with a more accurate spec (appended at the end of this email):
Model checking completed. No error has been found.
Estimates of the probability that TLC did not check all reachable states
because two distinct states had the same fingerprint:
calculated (optimistic): val =
Some nitpicking below:
On Mon, Jul 29, 2019 at 03:13:42PM +0100, Valentin Schneider wrote:
> specs.tla:
>
> MODULE specs
> EXTENDS Integers, Sequences, TLC
>
> CONSTANTS
> NR_WRITERS,
> NR_READERS,
> WRITER_TASK,
> READER_TASK
>
> WRITERS == {WRITER_TASK} \X (1..NR_WRI
2 matches
Mail list logo
