[tlaplus] Help with trivial spec: set generation

[Jeenu Viswambharan <jeenuv@xxxxxxxxx>]

Hi,

I'm having trouble writing up a rather trivial spec: fill a set that sum to a given total. Or rather, I'm verifying that the actions in spec generates such a set.

For example, given a goal 3, I'd expect either of these to be generated:

{<<0: 1>>, <<1: 1>>, <<2: 1>>}

{<<0: 1>>, <<1: 2>>}

{<<0: 2>>, <<1: 1>>}

{<<0: 3>>}

When running TLC, it complains about reaching deadlock, which I believe is when it reached the final state and no more states can be generated. That's fair enough, but how do I say it's not really deadlock, but is the final state and not error?

Also, in an attempt to get TLC to ignore this particular path and explore further, I specified -deadlock. Sometimes it complains about stuttering, and other times goes ahead with a runaway, seemingly infinite, counterexample. I'm unable to consistently reproduce the latter, despite specifying the seed and fp value printed by TLC (output in the repo).

I'd like to think there's something wrong with my spec, but am struggling to find what. I'd appreciate if someone can take a look and tell me what's wrong: https://bitbucket.org/jeenuv/test_spec/.

Thanks,

Jeenu

-- 
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/d1e6b7dc-11bb-4a79-84db-3df47c5edbfcn%40googlegroups.com.