PROBPLUGIN - No user feedback when TIME-OUT occurs during SETUP CONSTANTS

Description

When a time-out occurs during SETUP_CONSTANTS this is not reported to the user.
The dialog box should tell the user that a time-out has occurred.
Below is a project and a screenshot for animating train_ctx2.

The console for this example shows that a time-out occurs:

[(Output 62126)] % TIME OUT:
[(Output 62126)] % root
[(Output 62126)] % 2500
[(Output 62126)] % $setup_constants
[(Output 62126)] % time_out_for_node(root,$setup_constants,time_out)
[(Output 62126)] Solutions found for the following constants:
[(Output 62126)] fst/AVL.size=8
[(Output 62126)] lst/AVL.size=8
[(Output 62126)] nxt/AVL.size=8
[(Output 62126)] rtbl/AVL.size=32
[(Output 62126)] SIG/AVL.size=5
[(Output 62126)] blpt/AVL.size=3
[(Output 62126)] no_sol_for(lft)
[(Output 62126)] OpsSTAndIDs: []

!ENTRY de.prob.core 4 8 2014-01-27 10:55:04.515
!MESSAGE ProB could not find valid constants/variables. This might be caused by the animation settings (e.g., Integer range or deferred set size) or by an inconsistency in the axioms

Environment

None

Attachments

2

Gliffy Diagrams

Activity

Show:

Jenkins Build Server January 27, 2014 at 3:58 PM

SUCCESS: Integrated in

ProB_Tests_Linux64 #7741

Jenkins Build Server January 27, 2014 at 12:24 PM

SUCCESS: Integrated in

ProB_Tests_Linux32 #922
set state property timeout_occurred to true for every timeout, instead of just for invariant timeouts () (sebastian: rev a95b5cf08f6a001849e7edcbca8a93d94ad6a685)

  • src/eclipse_interface.pl

Jenkins Build Server January 27, 2014 at 11:42 AM

SUCCESS: Integrated in

ProB_Tests_Linux64 #7736

Fixed

Details

Assignee

Reporter

Priority

More fields

Created January 27, 2014 at 9:58 AM
Updated January 27, 2014 at 3:58 PM
Resolved January 27, 2014 at 10:20 AM