Weird behaviour which causes ERROR (Type.cpp:235): Operator requires boolean operands.

[Kroyers]

Hello,

while working with a PRISM model using Storm (1.7.0 built from source on Apple M1 chip) for my thesis I discovered a peculiar behaviour with Storm.

When a formula, which has int return type, is used in different formula which has a return type of boolean, Storm gives out the error "ERROR (Type.cpp:235): Operator requires boolean operands.".

The actual PRISM (4.7) model checker doesn't have a problem with this. Through more experimenting I discovered that Storm still managed to correctly evaluate the formula.

I'm attaching a simple PRISM model which can replicate the issue and contains the specific formulas I was using. I have also discovered, that moving the int formula formula current_min_leader_calc above the boolean formula formula leader_set manages to avoid the error. Unfortunately Github doesn't support the .pm file format so here is the raw text:

mdp

//formula current_min_leader_calc = min((A_mark?A_leader:8), (B_mark?B_leader:8));

formula leader_set = ((A_mark & A_leader = current_min_leader_calc | A_mark = false)?true:false) & ((B_mark & B_leader = current_min_leader_calc | B_mark = false)?true:false);

formula current_min_leader_calc = min((A_mark?A_leader:8), (B_mark?B_leader:8));

//It seems that using a formula, which has a int return type, inside a formula which has a boolean return type causes the error ERROR (Type.cpp:235): Operator requires boolean operands.
//Although it seems that the formula does work.
//BUT if the current_min_leader_calc is positioned above the leader_set formula (the commented formula), then there are no errors.

module whatever

    A_mark : bool init true;
    B_mark : bool init true;

    test1 : bool init false;

    A_leader : [0..10] init 1;
    B_leader : [0..10] init 1;

    [] A_mark = true & leader_set & test1 = false -> (test1'=true);
    //If A_mark is set to false, the model has only 1 state, which means the formula was evaluated correctly to false.
    //If A_mark is set to true, the model has 2 states, so test1 was updated to true, so the formula was evaluated correctly to true.

endmodule

[volkm]

I think the issue comes from the operator precedence. The expression which triggers the issue is A_mark & A_leader. Note that it is A_leader and not A_leader = current_min_leader_calc as expected.

As a workaround, I suggest to use brackets: A_mark & (A_leader = current_min_leader_calc). In addition, I suggest to also use brackets for the Boolean connectives ((A_mark & (A_leader = current_min_leader_calc)) | A_mark = false.

[tquatmann]

To be clear: the parsing is correct and everything works as expected. The only issue is that the error message appears, right?

I think it's some kind of "expected" parsing failure that occurs when trying to parse ((A_mark & A_leader = current_min_leader_calc ... before knowing about current_min_leader_calc. This parsing failure should be handled internally by parsing the expression again at a later point, but somehow the user is troubled with an error message about that.

I'll have a look into this as soon as I find the time. As far as I can see right now, the error message can safely be ignored.

[volkm]

In my (quick) debugging I found that the parsing seems to be incorrect. It seems to me that instead of trying to parse the sub-expression A_mark & A_leader = current_min_leader_calc the sub-expression A_mark & A_leader is parsed. This would be wrong. However, I might have overlooked or misinterpreted something. It would be good to take a closer look into the parsing tree if you find some time.

My suggestion for now is to use an abundance of brackets just to be on the safe side.