bmoth-mc bmoth issues - Githubissues

bmoth-mc / bmoth

Model Checker for (a subset of) classical B based on Z3

MIT License

9 stars 1 forks source link

issues

Newest

Newest Most commented Recently updated Oldest Least commented Least recently updated

FileChooser: Exceptions if LAST_DIR in BmothPreferences does not exist

#110 Jessypet closed 6 years ago
0
REPL Interface is confusing

#109 leuschel opened 6 years ago
1
Model Checking does not work for example

#108 leuschel opened 6 years ago
0
Dialog text for commands in menu "Other Checks"

#107 leuschel closed 6 years ago
0
Ambiguous ModelCheckingResult-type VERIFIED

#106 Jessypet closed 6 years ago
0
CliApplication: Default max_steps not applied

#105 Jessypet closed 6 years ago
1
Büchi Automaton of G {1=1} includes only accepting states

#104 wysiib closed 7 years ago
2
implementiert Tarjan's strongly connected components algorithm

#103 x-moe-x closed 7 years ago
5
implement state space exploration

#102 x-moe-x closed 7 years ago
1
implement equalAst(...) Method to enable Node being checked for equality

#101 x-moe-x closed 7 years ago
2
parse error with LTL formula including set arithmetic

#100 wysiib closed 7 years ago
0
Parser parses LTLPrefixOperatorNode as LTLBPredicateNode

#99 Mareikes closed 7 years ago
2
Generate Büchi automaton representing negated formula

#98 Jessypet closed 7 years ago
0
rewrite translation of x : NATURAL to x >= 0

#97 x-moe-x closed 7 years ago
0
implement LTL model checking

#96 wysiib closed 7 years ago
5
implement k-Induction based model checking

#95 wysiib closed 7 years ago
0
implement bounded model checking

#94 wysiib closed 7 years ago
0
Exceptions logged but not shown in the UI

#93 heinzware opened 7 years ago
0
Spurious counter-example found in the presence of deferred sets

#92 leuschel opened 7 years ago
4
Parse exception for machine

#91 leuschel closed 7 years ago
3
LiftDoesNotMoveTowardsFirstPressedButton throws Type Error

#90 wysiib closed 7 years ago
0
Machine: Initialisation does not apply constraintList

#89 x-moe-x closed 7 years ago
2
Parse only once

#88 wysiib closed 7 years ago
0
use mvvm pattern in ui

#87 wysiib closed 7 years ago
0
Model checker performance drop for CounterErr2

#86 leuschel opened 7 years ago
6
Exception when trying to open Cruise_finite1

#85 leuschel closed 7 years ago
10
Check for possible problems with Integer overflows

#84 Lunnaris01 closed 7 years ago
1
Pretty-printer for intervals

#83 Jessypet closed 7 years ago
1
Pretty-printer for nested declarations

#82 Jessypet closed 7 years ago
5
Display warnings in GUI

#81 dohan closed 7 years ago
1
Direct Product throws ClassCastException

#80 heinzware closed 7 years ago
0
clickingOptionsOpensDialog test fails

#79 heinzware closed 7 years ago
0
OptionControllerTest results are inconsistent

#78 heinzware closed 7 years ago
1
The BMothPreferences don't accept negative numbers

#77 heinzware closed 7 years ago
1
&, or: wrong operator precedence

#76 x-moe-x closed 7 years ago
6
UI: Button to stop model check

#75 Mareikes closed 7 years ago
9
have to select path everytime i click on save

#74 wysiib closed 7 years ago
1
SolutionFinder throws Exception if predicate is SAT without a model

#73 wysiib closed 7 years ago
2
Parser does not support ~ (relational inverse)

#72 leuschel closed 7 years ago
2
REPL exception for 3>2

#71 leuschel closed 7 years ago
3
REPL exception for expressions

#70 leuschel closed 7 years ago
0
REPL needs a pretty-printer

#69 wysiib closed 7 years ago
2
SolutionFinder::findSolutions(...) returns multiple models for the same associated State

#68 x-moe-x closed 7 years ago
6
z3 power function leads to nonlinear real arithmetic, colliding with quantifier formula

#67 x-moe-x closed 7 years ago
5
z3 finds counter example for exponentiation when there is none

#66 Mareikes opened 7 years ago
3
Separate check item for "check everything"

#65 wysiib closed 7 years ago
2
Add preference to set Z3 timeout

#64 wysiib closed 7 years ago
1
Preferences create Warning on Windows

#63 Lunnaris01 closed 7 years ago
1
we can divide by zero öÖ

#62 wysiib closed 7 years ago
0
Parser does not show line number of syntax error

#61 leuschel closed 7 years ago
0