Skip to content

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