Forgetting "var" on a field in temporal mode can lead to a silent failure #182
Description
In this example:
#lang forge
option problem_type temporal
one sig Counter {
-- Forge 2.1 *silently fails* if we forget "var" here
count: one Int
}
pred init { Counter.count = 0}
pred move { Counter.count' = add[Counter.count, 1] }
test expect {
-- Confirm extension w/o traces pred:
move_1: {init and move} for 3 Int is sat
}
I have neglected to declare count as var, and so it cannot vary over time. The move predicate asks for it to vary, however, which seems to indicate a mismatch in intent. I'd like to see an error here. In this example, it would be a straightforward scan within a (prime ...) node to confirm that at least something within is declared var.
Requires discussion, however.