Unsupported property warning printed 2 times.
Description:
In the code snippet below, the unsupported property warning is printed 2 times.
This happens because the test property has been added twice to the list of properties for the model, with different quantifiers each time.
Property: property test = Pmin(state == 3) > 0;
*@ModelCheckingAnalysisEngine.902*
model.Properties = {Modest.Expressions.Property[2]}
[0] -> property "test" = filter(∀, Pmin(false) > 0, initial)
[1] -> property "test" = filter(∃, Pmin(false) > 0, initial)
Output:
(00:00) 0..
Preparing model checking...
server_2.modest: info: server_2 is an MDP model.
(01:52) 0....
Preprocessing properties...
server_2.modest:(3,10): warning: Skipping unsupported property "test".
server_2.modest:(3,10): warning: Skipping unsupported property "test".
server_2.modest: error: No properties to check.
Model:
action start, safe, risk, finish, close, reset;
int state = 0;
property test = Pmin(state == 3) > 0; // error gets printed 2 times
process Server(int state)
{
if(state == 0) { start {= state = 1 =} }
else if(state == 1) {
alt {
:: safe palt {
:6: tau {= state = 0 =}
:3: tau {= state = 2 =}
:1: tau {= state = 3 =}
}
:: risk palt {
:5: tau {= state = 2 =}
:5: tau {= state = 3 =}
}
}
}
else if(state == 2) {finish}
else { //state == 3
alt {
:: close {= state = 3 =}
:: reset {= state = 0 =}
}
};
Server(state)
}
Server(0)