Commits

Nadia Polikarpova committed 7768bd7 Draft

Edited online

Comments (0)

Files changed (1)

 The above command will try to find one valid execution of procedure {{{Main}}} in SumMax.bpl and upon its termination display the values of all global entities and parameters of {{{Main}}} that were read or written during the execution.
 An alternative entry point can be specified through the {{{--proc}}} flag.
 
-You have control over various parameters of the non-deterministic behavior, such as the //branching factor// (the maximum number of possibilities to consider at every choice point), the way integer values are generated (exhaustively or randomly), the maximum number of executions to try and to display, as well as filtering options for executions.
+You have control over various parameters of the non-deterministic behavior, such as the //branching factor// (the maximum number of possibilities to consider at every choice point), the way integer values are generated (exhaustively or randomly), the limit on the number of executions to try and to display, as well as filtering options for executions.
+
+By default Boogaloo filters out invalid executions (those that end with an assumption violation). If you completely disable filtering then the number of executions to try and to display become the same thing. If you remove the limit on the number of executions, it will only be bounded by the branching factor. So if you further set the branching factor to "unbounded" the interpreter will keep producing new executions infinitely – that is, if you program involves at least one non-deterministic choice of an integer value.    
 
 ===Exhaustive testing===