Open issues

Unsat Core computation should provide feedback
PROB2UI-346
Cannot open B machines when a warning is produced
PROB2UI-345
Unsat Core Display when SETUP_CONSTANTS fail
PROB2UI-341
Add support for Z models
PROB2UI-340
StackOverflow in Magic Layout for CAN_BUS_tlc
PROB2UI-339
Exception when saving a trace file
PROB2UI-337
Display of machine in editor wrong: overlapping words
PROB2UI-335
The Trace Replay sometimes seems to check output parameters on the wrong state
PROB2UI-329
Investigate why ProB2-UI needs a higher TIME_OUT to work
PROB2UI-324
B editor should support highlighting for languages other than classical B
PROB2UI-319
B editor tries to highlight non-classical-B code using the classical B lexer
PROB2UI-318
Replaying long model checking counter examples takes some time
PROB2UI-311
Cluster Nodes
PROB2UI-301
Development of Magic Layout
PROB2UI-298
Change state view to use the same internal mechanism that is used in Rodin
PROB2UI-293
Investigate UI performance
PROB2UI-291
Adapt Display of LTL Formulas
PROB2UI-284
Use Unicode in State View
PROB2UI-279
Extend find valid state command with checkbox for using current constants values
PROB2UI-278
Allow expansion of formulas in state viewer
PROB2UI-277
Try and reuse probcli when loading or re-loading a model
PROB2UI-276
Show origin of entries in the state view
PROB2UI-275
Display description as hover tooltip in state view
PROB2UI-274
Operations view shows too many operations which are not top-level
PROB2UI-264
ANIMATION_FUNCTION images path
PROB2UI-248
Settings are reset when a new ProB 2 version is released
PROB2UI-243
Add symbolic feasibility command
PROB2UI-241
Make a version of the UI with a bundled JRE
PROB2UI-218
State view: INVARIANTS heading should be red when one invariant false
PROB2UI-188
Cannot save/replay CSP traces
PROB2UI-164
Cannot quit ProB2-UI
PROB2UI-323
After Model Checking the Dot Windows pops in front
PROB2UI-272
B console doesn't scroll to the bottom when a long result causes the scrollbar to appear
PROB2UI-244
Shortcut "Ctrl++" doesn't work
PROB2UI-208
Shortcut for 'Zoom Out' doesn't work
PROB2UI-204
issue 1 of 35

Unsat Core computation should provide feedback

Description

It seems that currently the unsat core is computed automatically, leading to delays in
user feedback.
Before computing the unsat core, the user should obtain some feedback that
the PROPERTIES are inconsistent.
Possibly a dialog could pop up or a button could be put into the state view to compute
the unsat core only upon demand, as it can be quite expensive to compute.

Example: public_examples/B/UnsatCore/UnsateTest1.mch

Status

Assignee

Fabian Vu

Reporter

Michael Leuschel

Labels

None

Priority

Major