External Model Checking

Description

Implement a max queue size, if the queue becomes larger save sucessor states to disk. Maybe report sum of internal and external states to master or (better) a tuple of values.

Implement a new termination cycle that instructs the workers to externalize new states when maxstates reached (in queue) and collect them on termination.

Environment

None

Activity

Show:
Jenkins Build Server
January 30, 2013, 5:30 PM

Integrated in

ProB_TclTk_Windows #148
fixes and works on (Revision 12910)

Result = SUCCESS
koerner :
Files :

  • /trunk/prolog/extensions/zmq/external.c

  • /trunk/prolog/extensions/zmq/external.h

  • /trunk/prolog/extensions/zmq/worker.c

Jenkins Build Server
January 31, 2013, 3:38 PM

Integrated in

ProB_TclTk_Linux #5410
(Revision 12920)

Result = SUCCESS
koerner :
Files :

  • /trunk/prolog/extensions/zmq/external.c

  • /trunk/prolog/extensions/zmq/master.c

  • /trunk/prolog/extensions/zmq/queue.c

  • /trunk/prolog/extensions/zmq/queue.h

  • /trunk/prolog/extensions/zmq/worker.c

Jenkins Build Server
January 31, 2013, 7:53 PM

Integrated in

ProB_TclTk_Windows #150
(Revision 12920)

Result = SUCCESS
koerner :
Files :

  • /trunk/prolog/extensions/zmq/external.c

  • /trunk/prolog/extensions/zmq/master.c

  • /trunk/prolog/extensions/zmq/queue.c

  • /trunk/prolog/extensions/zmq/queue.h

  • /trunk/prolog/extensions/zmq/worker.c

Jenkins Build Server
February 14, 2013, 1:42 PM

Integrated in

ProB_Tests_Linux_No_Parallel #17

Result = SUCCESS

Philipp Koerner
October 21, 2014, 9:03 AM

This already is implemented. Also, model checking is durable now anyway.

Fixed

Assignee

Philipp Koerner

Reporter

Jens Bendisposto

Priority

Major