search

hhu-stups / prob-issues

ProB issues (for probcli, ProB Tcl/Tk, ProB2, ProB2UI)
6 stars 0 forks source link

LTL Model Checking does not provide feedback #239

Open favu100 opened 2 years ago

favu100 commented 2 years ago

Somehow, the LTL model check does not provide feedback when model checking. The statistics are only updated when expanding the stats view.

Somehow, the LTL model check seems to take more time than previously and cannot be interrupted:

14:16:33.775 [ProB Output Logger for instance 1309736f] INFO de.prob.cli.ProBInstance - raise_prolog_exception!
14:16:33.799 [ProB Output Logger for instance 1309736f] INFO de.prob.cli.ProBInstance - ! user_interrupt_signal
14:16:33.813 [ProB Output Logger for instance 1309736f] INFO de.prob.cli.ProBInstance - ! goal:  clpfd_interface:(1 in_set _887557)
14:19:15.951 [ProB Output Logger for instance 1309736f] INFO de.prob.cli.ProBInstance - 
14:19:15.951 [probcli command executor] DEBUG de.prob.animator.CommandProcessor - Yes: Errors->[] R->ok 
14:19:15.951 [ProB Output Logger for instance 1309736f] INFO de.prob.cli.ProBInstance - ALL OPERATIONS COVERED
14:19:15.952 [ProB Output Logger for instance 1309736f] INFO de.prob.cli.ProBInstance - Safety model checker progress: 35.1% % of 1935 states processed, 49813 transitions (delta = 30.2 sec)
14:19:15.952 [ProB Output Logger for instance 1309736f] INFO de.prob.cli.ProBInstance - Safety model checker progress: 59.4% % of 2394 states processed, 114156 transitions (delta = 32.5 sec)
14:19:15.952 [probcli command executor] DEBUG de.prob.cli.ProBConnection - get_error_messages_with_span_info(Errors),true.
14:19:15.952 [ProB Output Logger for instance 1309736f] INFO de.prob.cli.ProBInstance - Safety model checker progress: 57.6% % of 3211 states processed, 152889 transitions (delta = 18.9 sec)
14:19:15.952 [ProB Output Logger for instance 1309736f] INFO de.prob.cli.ProBInstance - Safety model checker progress: 64.1% % of 3211 states processed, 169494 transitions (delta = 12.1 sec)
14:19:15.952 [ProB Output Logger for instance 1309736f] INFO de.prob.cli.ProBInstance - Safety model checker progress: 74.0% % of 3217 states processed, 198513 transitions (delta = 17.6 sec)
14:19:15.952 [ProB Output Logger for instance 1309736f] INFO de.prob.cli.ProBInstance - Safety model checker progress: 85.4% % of 3243 states processed, 233444 transitions (delta = 20.0 sec)
14:19:15.952 [ProB Output Logger for instance 1309736f] INFO de.prob.cli.ProBInstance - Safety model checker progress: 97.3% % of 3297 states processed, 273268 transitions (delta = 20.4 sec)
14:19:15.952 [ProB Output Logger for instance 1309736f] INFO de.prob.cli.ProBInstance - Safety model checker progress: 98.4% % of 3297 states processed, 276453 transitions (delta = 10.3 sec)
14:19:15.952 [ProB Output Logger for instance 1309736f] INFO de.prob.cli.ProBInstance - All open states visited! States analysed: 3289
14:19:15.952 [ProB Output Logger for instance 1309736f] INFO de.prob.cli.ProBInstance - % Overall Checking Time: 135226 ms
leuschel commented 2 years ago

Bei LTL gibt es aktuell prinzipiell kein Feedback während des Laufens: der LTL Algorithmus arbeitet Depth-First und kann nicht einfach unterbrochen werden (um eine Antwort an Java zu schicken) und später wieder aufgenommen werden. Aber, ich hatte dafür vor einiger Zeit die Call-Back Möglichkeit im Java-Prolog Protokoll vorgesehen; Prolog könnte demnach hin und wieder Info-Pakete zurückschicken und sofort mit dem LTL Check weitermachen. Man müsste dafür auf ProB2 Seite diese Call-Backs unterstützen.