PROBPLUGIN - No user feedback when TIME-OUT occurs during SETUP CONSTANTS
Description
Environment
None
Attachments
2
Gliffy Diagrams
Activity
Show:

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

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
Fixed
Details
Details
Assignee

Reporter

Priority
More fields
Story Points, Original estimate
More fields
Story Points, Original estimateCreated January 27, 2014 at 9:58 AM
Updated January 27, 2014 at 3:58 PM
Resolved January 27, 2014 at 10:20 AM
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