Duplicate properties get skipped silently
At the moment, duplicate properties are skipped silently. We should inform the user that a given property is being skipped.
This could be especially useful in the case the user doesn't know 2 properties are equivalent (for example, in the case that we rewrite a property underwater). I encountered this when writing some very basic properties for bug hunting, and to my surprise not all properties showed up on the output.
Model:
property p_1 = Pmin(<> true);
property p_2 = Pmin(<> true);
property p_3 = Pmin(<> false);
process RandomWalk()
{
int i;
tau palt {
:6: {= i = (i + 1) % 5 =}; RandomWalk()
:4: {= =}; RandomWalk()
}
}
RandomWalk()
Output:
[...]
+ State space exploration
State size: 1 bytes
States: 1
Transitions: 1
Branches: 2
Rate: 15 states/s
Time: 0.1 s
+ Property p_1
Probability: 1
Bounds: [1, 1]
Time: 0.0 s
+ Value iteration
Final error: 0
Iterations: 1
Time: 0.0 s
+ Property p_3
Probability: 0
Bounds: [0, 0]
Time: 0.0 s
+ Value iteration
Final error: 0
Iterations: 1
Time: 0.0 s
Edited by Hans van der Laan