Minimal output format forgets endline after printing boolean variables.
As stated in the title, the minimal output format doesn't add a newline after it prints a boolean to the output file.
Output:
"p_1": 1
"p_2": 0
"p_3": True"p_4": False"p_5": 0
"p_6": False"p_7": 1
Model:
action start, safe, risk, finish, close, reset;
int global_state = 0;
property p_1 = Pmin(<> true);
property p_2 = Pmax(<> false);
property p_3 = Pmin(<> true) > 0;
property p_4 = Pmin(<> false) > 0;
property p_5 = Pmin(<> false);
property p_6 = Pmin(<> false) == 1;
property p_7 = Pmax(<> true);
process Server(int state)
{
alt {
:: when(state == 0) start {= state = 1, global_state = 1 =}
:: when(state == 1) alt {
:: palt {
:6: safe {= state = 0, global_state = 0 =}
:3: safe {= state = 2, global_state = 2 =}
:1: safe {= state = 3, global_state = 3 =}
}
:: palt {
:5: risk {= state = 2, global_state = 2 =}
:5: risk {= state = 3, global_state = 3 =}
}
}
:: when(state == 2) finish {= state = 2, global_state = 2 =}
:: when(state == 3)
alt {
:: close {= state = 3, global_state = 3 =}
:: reset {= state = 0, global_state = 0 =}
}
};
Server(state)
}
Server(0)