All work
- ProB hangs after starting model checkPROBPLUGIN-121Resolved issue: PROBPLUGIN-121Jens Bendisposto
- Export to ProB Classic does not workPROBPLUGIN-120Jens Bendisposto
- Internal Error instead of properly reported well-definedness errorPROBPLUGIN-119Jens Bendisposto
- ModelCheckingDialog does not store user selectionPROBPLUGIN-118Resolved issue: PROBPLUGIN-118Sebastian Krings
- List theory does not work in ProB Plug-inPROBPLUGIN-117Jens Bendisposto
- Rendering of ... is strangePROBPLUGIN-115Jens Bendisposto
- No feedback when timeout in INITIALISATIONPROBPLUGIN-114Jens Bendisposto
- Check Documentation for ProB 1PROBPLUGIN-116Jens Bendisposto
- Error messages in Animator after Disprover runPROBPLUGIN-113Resolved issue: PROBPLUGIN-113Jens Bendisposto
- LTL Model Check fails when number of new nodes exceededPROBPLUGIN-112Resolved issue: PROBPLUGIN-112Jens Bendisposto
- Number of variables in a pre-post predicatePROBPLUGIN-111Resolved issue: PROBPLUGIN-111Jens Bendisposto
- LTL Counterexample is not displayed in the HistoryPROBPLUGIN-110Daniel Plagge
- LTL does not work anymorePROBPLUGIN-109Resolved issue: PROBPLUGIN-109Daniel Plagge
- BMotionStudio throws cast exception in Rodin3PROBPLUGIN-108Resolved issue: PROBPLUGIN-108Lukas Ladenberger
- Disprover should report needed hypotheses back to RodinPROBPLUGIN-107Sebastian Krings
- Allow to submit POsPROBPLUGIN-106Resolved issue: PROBPLUGIN-106Sebastian Krings
- input fields for units / symbolic are not available anymorePROBPLUGIN-104Resolved issue: PROBPLUGIN-104Sebastian Krings
- Assertion Checking: No feedback after model checking runPROBPLUGIN-103Resolved issue: PROBPLUGIN-103Jens Bendisposto
- NullPointer Exception when Full Coverage in Model Checking reachedPROBPLUGIN-102Resolved issue: PROBPLUGIN-102Jens Bendisposto
- On animating a machine with pro-B, I get an error which says "Residue: root: '$partial_setup_constants: context = ERROR CONTEXT: OPERATION: $partial_setup_constants, state ID: root, state: root;"PROBPLUGIN-100Resolved issue: PROBPLUGIN-100Jens Bendisposto
- Variants trigger a translation errorPROBPLUGIN-99Resolved issue: PROBPLUGIN-99Sebastian Krings
- Invarants occurr multiple times in the translated modelPROBPLUGIN-97Resolved issue: PROBPLUGIN-97Daniel Plagge
- PROBPLUGIN - No user feedback when TIME-OUT occurs during SETUP CONSTANTSPROBPLUGIN-96Resolved issue: PROBPLUGIN-96Jens Bendisposto
- Disprover: Free identifiers in the proof are not handled correctlyPROBPLUGIN-95Resolved issue: PROBPLUGIN-95Sebastian Krings
- PROBPLUGIN: ProB Animate Menu for Shared Event Composed MachinePROBPLUGIN-94Resolved issue: PROBPLUGIN-94Sebastian Krings
- PROBPLUGIN - Disprover does not work with Theory PluginPROBPLUGIN-93Resolved issue: PROBPLUGIN-93Sebastian Krings
- PROBPLUGIN Theory Support Bug for ParametersPROBPLUGIN-92Resolved issue: PROBPLUGIN-92Michael Leuschel
- PROBPLUGIN - State View Expression does not allow Theory Plugin operatorsPROBPLUGIN-91Resolved issue: PROBPLUGIN-91Michael Leuschel
- PROBPLUGIN - LTL Counter-Example View - cannot display a counter examplePROBPLUGIN-90Resolved issue: PROBPLUGIN-90Michael Leuschel
- Error launching ProB Animation (If parent machine being extended has theorems in guards)PROBPLUGIN-89Resolved issue: PROBPLUGIN-89Jens Bendisposto
- PROBPLUGIN - ProB 1 for Rodin - Execute with Custom Guard IssuesPROBPLUGIN-88Resolved issue: PROBPLUGIN-88Jens Bendisposto
- PROB - ProB for Rodin cannot start when special character in pathPROBPLUGIN-87Resolved issue: PROBPLUGIN-87Sebastian Krings
- Closing the Events View and reopening it again throws a NullPointerExceptionPROBPLUGIN-84Resolved issue: PROBPLUGIN-84Sebastian Krings
- Translation failsPROBPLUGIN-80Resolved issue: PROBPLUGIN-80Sebastian Krings
- "becomes such as" operation causes unhandled loop exceptionPROBPLUGIN-79Resolved issue: PROBPLUGIN-79Jens Bendisposto
- Observer:Simple value Display ControlPROBPLUGIN-78Resolved issue: PROBPLUGIN-78Lukas Ladenberger
- PROB Rodin - Export error message upon warnings misleadingPROBPLUGIN-75Resolved issue: PROBPLUGIN-75Jens Bendisposto
- ProB does not release memory after model checkingPROBPLUGIN-74Resolved issue: PROBPLUGIN-74Joy Clark
- Update Wiki (Disprover / Symbolic Constants / Units)PROBPLUGIN-73Resolved issue: PROBPLUGIN-73Sebastian Krings
- ProB for Rodin should support theorems in guardsPROBPLUGIN-72Resolved issue: PROBPLUGIN-72Michael Leuschel
- memory leakPROBPLUGIN-71Resolved issue: PROBPLUGIN-71Jens Bendisposto
- memory leak triggered by Context contentsPROBPLUGIN-70Resolved issue: PROBPLUGIN-70Michael Leuschel
- Create way to export Event-B files for ProB 2.0PROBPLUGIN-69Resolved issue: PROBPLUGIN-69Jens Bendisposto
- Outdated: http://wiki.event-b.org/index.php/DisproverPROBPLUGIN-68Resolved issue: PROBPLUGIN-68Sebastian Krings
- Command for checking initialised status is out of datePROBPLUGIN-67Resolved issue: PROBPLUGIN-67Joy Clark
- Disprover unable to type variables of refined machinesPROBPLUGIN-66Resolved issue: PROBPLUGIN-66Sebastian Krings
- Translation Crashes if Symbolic Constants Plugin is not installedPROBPLUGIN-64Resolved issue: PROBPLUGIN-64Sebastian Krings
- ProB Rodin: cannot animate machine m1 - export for ProB classic silently failsPROBPLUGIN-63Resolved issue: PROBPLUGIN-63Sebastian Krings
- Change Model checking options to fit with Prolog refactoringPROBPLUGIN-62Resolved issue: PROBPLUGIN-62Jens Bendisposto
- Units not translated in contextsPROBPLUGIN-58Resolved issue: PROBPLUGIN-58Sebastian Krings
50 of 96
ProB hangs after starting model check
Fixed
Description
Environment
OSX 10.13.6
Rodin 3.4
ProB 3.0.9.201803300836 (i do not recognise the versions in the dropdown)
Attachments
2
Created October 18, 2018 at 2:12 PM
Updated November 28, 2018 at 12:28 PM
Resolved November 28, 2018 at 12:28 PM
Activity
Show:
Colin SnookNovember 3, 2018 at 1:24 PM
I have now checked the nightly build and it works well on my iUML-B project, even starting the model check from a state machine animation which has always been unreliable in the past. Maybe it has fixed some of the other problems I had.
Colin SnookOctober 23, 2018 at 11:25 PM
Yes, it seems to work ok now (running from source).
Thanks for the quick fix!
Jens BendispostoOctober 23, 2018 at 4:45 PM
I think the issue is now fixed. Can you please verify? @Colin Snook
Michael LeuschelOctober 23, 2018 at 1:11 PMEdited
Above I attach a threaddump obtained by VisualVM started by typing "jvisualvm" in the console.
Maybe somebody else can see whether this dump is helpful and hints at the source of the problem (deadlock ???)
Michael LeuschelOctober 23, 2018 at 1:10 PM
I can confirm that
the issue does not appear in Rodin 3.3 with the latest plugin
only seems to appear when a counter example is found by the model checker and the B machine is not initialised.
After starting model check on m0 in the attached project, Rodin never returns and has to be force quit.
The Event-b contains iUML-B statemachines which generated some of the Event-B.
I have tried importing the project into a fresh install of Rodin with only ProB installed - still hangs
In Rodin 3.3 - model check works ok.. it does NOT hang.