utwente-fmt / vercors

The VerCors verification toolset for verifying parallel and concurrent software
https://utwente.nl/vercors
Mozilla Public License 2.0
51 stars 24 forks source link

Add challenge 3 from the verifyThis 2019 challenge #1167

Closed sakehl closed 2 months ago

sakehl commented 3 months ago

Add example for solving challenge 3 from the verifyThis 2019 challenge.

Also add the possibility to test with a specific flag. Needed since otherwise the challenge does not verify.

bobismijnnaam commented 3 months ago

Preemptive apologies for not understanding your use case. I have a few tests that use flags already, see here: https://github.com/utwente-fmt/vercors/blob/72735981dd3ab612f93aa918d6b152f80dee9d7e/test/main/vct/test/integration/examples/VeyMontExamplesSpec.scala#L12 Does that work for you? If that is somehow not what you need please ignore my comment :)

sakehl commented 3 months ago

Ohhh thanks a lot, that works! I changed it