prismmodelchecker / prism

The main development version of the PRISM model checker.
http://www.prismmodelchecker.org/
GNU General Public License v2.0
157 stars 72 forks source link

Properties are checked twice for each undefined boolean constants #232

Closed merkste closed 1 year ago

merkste commented 1 year ago

If a model contains an undefined boolean constant that is assigned true or false at the command line, all properties are checked twice. Consider the following example:

// A simple model that depends on an undefined boolean constant
mdp

const bool flag;

module Boolean
  b : bool init flag;
endmodule

and the command line

prism example.prism -pf b -const flag=false
davexparker commented 1 year ago

Fixed by #233.