Allow to provide additional target predicate for the symbolic model checking command

hhu-stups / prob-issues

ProB issues (for probcli, ProB Tcl/Tk, ProB2, ProB2UI)

6 stars 0 forks source link

Allow to provide additional target predicate for the symbolic model checking command #32

Open leuschel opened 3 years ago

leuschel commented 3 years ago

It would be nice to be able to provide an additional target predicate for the symbolic / aka bounded model checking commands.

Screenshot 2021-02-23 at 15 22 57

Also, currently only one of the BMC commands is available. ProB also provides a BMC algorithm which is a special case of the test-case generation algorithm. This one is typically much better (it uses an enabling analysis) and does allow specifying a target predicate.

favu100 commented 3 years ago

Is there a command in prob2_interface to invoke the BMC algorithm which is based on the test-case generation algorithm?