ProB2UI CTL model check does not work with XTL files

hhu-stups / prob-issues

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

6 stars 0 forks source link

ProB2UI CTL model check does not work with XTL files #352

Closed leuschel closed 2 months ago

leuschel commented 2 months ago

There is a result_is_not_ground exception. It seems like the Java side is parsing the CTL formula assuming that it is for a B model.

[DEBUG] Sending: prob2_do_ctl_modelcheck(ag(not(ap(enabled(bop(oppattern(pos(-1,-1,1,8,1,13),start,[])))))),[max_new_states(-1),mode(init)],R,CE),true. [INFO] % No B machine available for [INFO] % b_get_machine_operation(start,_377941,_377943,_377931,_377933,_377935) [INFO] exception(make_call/3, result_is_not_ground). [ERROR] Unhandled exception during checking

leuschel commented 2 months ago

Maybe commit edd4612099575d0e11946be59e8d0cf72b4dfc55 in prob_prolog is already enough to fix this.

iTitus commented 2 months ago

It seems to work now