tnelson / Forge

Forge: A Tool and Language for Teaching Formal Methods
https://forge-fm.org/
MIT License
67 stars 9 forks source link

Temporal forge needs `max_tracelength` to be set before `min_tracelength` #274

Open dominicmkennedy opened 2 months ago

dominicmkennedy commented 2 months ago

Temporal Forge code:

#lang forge/temporal

option min_tracelength 6
option max_tracelength 6

Error message:

Cannot set min_tracelength to 6 because min_tracelength cannot be greater than max_tracelength. Current max_tracelength is 5.
tnelson commented 2 weeks ago

I think the issue title is slightly off, since it refers to max twice, rather than min and max.

But setting that aside, this is annoying, I agree. But the problem is one of atomicity. Without the following max_tracelength statement, the first would put the system in a state that violated the invariant max_tracelength >= min_tracelength. Forge doesn't do lookahead, and there's not at present a way to make atomic changes to multiple options at once. I'm happy to take suggestions, though.