dehnert
|
91e177028d
|
Started refactoring explicit model generator of PRISM models
Former-commit-id: 4ea82670d0
|
11 years ago |
dehnert
|
5e37c09fc0
|
Fixed some bugs.
Former-commit-id: dce463081d
|
11 years ago |
dehnert
|
231d2223a9
|
Model building works again (more or less)
Former-commit-id: fa6843fcdc
|
11 years ago |
dehnert
|
8ec362bb7d
|
Started debugging new model generation.
Former-commit-id: 704a7957f2
|
11 years ago |
dehnert
|
6f2916d557
|
Adapted the explicit model generator to the new hash map. Surprise: doesn't work yet.
Former-commit-id: dc60f568bf
|
11 years ago |
dehnert
|
30f78b0a99
|
Intermediate commit. Started improving explicit model adapter performance.
Former-commit-id: 8a4aa64ac6
|
11 years ago |
dehnert
|
53196f5610
|
Created bit vector hash map and some necessary bit vector methods.
Former-commit-id: 4a9946a743
|
11 years ago |
dehnert
|
ab0caf79e8
|
Replaced action names by indices in PRISM programs.
Former-commit-id: e66820c247
|
11 years ago |
dehnert
|
3260a6203c
|
Started improving performance of explicit model generation.
Former-commit-id: 318a97aedc
|
11 years ago |
dehnert
|
994250a697
|
Fixed missing ifdefs.
Former-commit-id: 1e95658a8f
|
11 years ago |
dehnert
|
650770148d
|
Main now compiles again, yay.
Former-commit-id: cc1307aea8
|
11 years ago |
dehnert
|
b37e009168
|
Further steps to new expressions.
Former-commit-id: 4396857eff
|
11 years ago |
dehnert
|
ee9533e586
|
Started working on making the main executable build again.
Former-commit-id: 9aaad15b9f
|
11 years ago |
dehnert
|
2eeaa06d76
|
Z3 runs fine again.
Former-commit-id: a725a33f01
|
11 years ago |
dehnert
|
ed74392f0d
|
Another intermediate commit.
Former-commit-id: 37585dbfa0
|
11 years ago |
dehnert
|
99d9a9710d
|
Further steps to make everything work again.
Former-commit-id: 3f45a49dab
|
11 years ago |
dehnert
|
983a7d78c2
|
Further work on expressions.
Former-commit-id: 4774f0136d
|
11 years ago |
dehnert
|
fff18f2789
|
Intermediate commit (refactoring expressions).
Former-commit-id: e7cc7e95c2
|
11 years ago |
dehnert
|
809217c359
|
Refactored some parts of expressions. In particular, visitors now can return anything they want by using boost::any.
Former-commit-id: 0f6af138ae
|
11 years ago |
dehnert
|
85a4376e39
|
Now StoRM can be properly compiled without support for MathSAT if needed.
Former-commit-id: 28da4f5ed8
|
11 years ago |
dehnert
|
7b8c382303
|
Added tests for Mathsat expression adapter.
Former-commit-id: 4f8ef4c3c3
|
11 years ago |
dehnert
|
f54b5671ea
|
Done refactoring MathSAT expression adapter.
Former-commit-id: 6edb98b86c
|
11 years ago |
dehnert
|
a061cdbed8
|
Started refactoring MathSAT adapter.
Former-commit-id: 93b1fdedb3
|
11 years ago |
dehnert
|
84bfd58884
|
Minor refactoring of Z3 expression adapter.
Former-commit-id: b31ae87a98
|
11 years ago |
dehnert
|
81571878f7
|
Further refactoring of MathSAT solver.
Former-commit-id: 317a9f9545
|
11 years ago |
dehnert
|
6eb415f87f
|
Tests for MathSAT now run through on Mac OS.
Former-commit-id: 9f6cf0af6a
|
11 years ago |
dehnert
|
d8be64f0d7
|
Started on making MathSatSmtSolver work properly.
Former-commit-id: c370658b26
|
11 years ago |
dehnert
|
3231ea6c06
|
Moved to new macros.
Former-commit-id: d97c947c22
|
11 years ago |
dehnert
|
79798e2cb1
|
Fixed the reward-issue even harder.
Former-commit-id: 2ca1c229e1
|
11 years ago |
dehnert
|
a7bce9e520
|
Removed debug output and fixed the reward issue a bit more.
Former-commit-id: ecbbeff14e
|
11 years ago |
dehnert
|
7cd0dfe8b0
|
Fixed an issue regarding the reward model generation.
Former-commit-id: 237acf99f9
|
11 years ago |
dehnert
|
2f20abf47f
|
The user can now select on the command line which reward model of a symbolic model is to be used (as a second [optional] argument to --symbolic).
Former-commit-id: 02f998e5dd
|
11 years ago |
David_Korzeniewski
|
25d87bae06
|
Builds fine, still no tests yet
Former-commit-id: 3d9d85679a
|
11 years ago |
David_Korzeniewski
|
56edf1e126
|
Initial MathSat integration.
Expression adapter, solving, unsat assumptions implemented
cmake and tests missing
allsat and interpolation not yet implemented
Former-commit-id: 5177775fbe
|
11 years ago |
dehnert
|
e49814d391
|
Modified pctl/csl/ltl options to now take formulas instead of files. Prefixed the macros with STORM_. Moved these macros into a file in the utilities. Modified architecture of the exception classes slightly. Threw away all the contents of main(). This will now be build from scratch.
Former-commit-id: 89d94f7957
|
11 years ago |
dehnert
|
433bae1156
|
Switched from an option to fix deadlocks to an option to not fix the deadlocks. Hence, deadlocks are now fixed by default unless otherwise requested.
Former-commit-id: 9434215807
|
11 years ago |
dehnert
|
1cd01e3f28
|
Adapted all places that are accessing the settings to the new interface. It now compiles again with a lot of linker errors (because of method bodies that are not yet present).
Former-commit-id: 01a33e479d
|
11 years ago |
dehnert
|
9ad12616e2
|
Renamed files in settings module a bit. Started on the pseudo-modular module-settings.
Former-commit-id: b3162aa86b
|
11 years ago |
dehnert
|
96e1f8faf9
|
Renamed Settings class to SettingsManager.
Former-commit-id: 2b33f4c8d0
|
11 years ago |
dehnert
|
9569426c86
|
Moved option registration to the settings class (so it's not deceentralized any longer). This enables to build storm as a library and on top of that build some exectuables, which saves a lot of compile time as soon as several targets have to be built or one switches between targets.
Former-commit-id: 69e0d526c7
|
11 years ago |
dehnert
|
418ce8b625
|
Fixed some problems related to the memory-mapped file.
Former-commit-id: 68225d8006
|
11 years ago |
dehnert
|
fff4e61fc3
|
Changed interface of matrix builder slightly to be able to also not force the resulting matrix to certain dimensions, but merely to reserve the desired space.
Former-commit-id: e36d05398e
|
11 years ago |
dehnert
|
aecd0e3cb8
|
Made Storm compile again without Z3: guarded some header inclusions and function definitions/implementations. Also guarded the tests that require certain libraries (like Gurobi, glpk, Z3), so that tests do not fail any more when the libraries are not available.
Former-commit-id: 307036e25c
|
11 years ago |
dehnert
|
e2c2177dca
|
Adapted MaxSAT-based minimal command set generator to some recent changes to make it work again.
Former-commit-id: 8f8c33b920
|
11 years ago |
dehnert
|
40c698af90
|
Some fixes to make new SMT framework compile with clang under Mac OS (includes fixes to some initializiation ordering warnings). Bugfix for PRISM parser to correctly handle formulas.
Former-commit-id: d513476066
|
11 years ago |
David_Korzeniewski
|
ee89065b07
|
Fixed type error on gcc and clang (int_fast64_t is not the same type as on msvc)
Former-commit-id: 06f4ba0f60
|
11 years ago |
David_Korzeniewski
|
93c03fff3f
|
Fixed order of checks in Z3ExpressionAdapter, fixed missing override of isVariable in VariableExpression, removed unnecessary exception in Z3SmtSolver model generation
Former-commit-id: ca5f876655
|
11 years ago |
David_Korzeniewski
|
a0319cb6e7
|
Model Generation and Tests for translating from z3 to storm
translating from z3 to storm has still some errors
Former-commit-id: 2a46b6c615
|
11 years ago |
David_Korzeniewski
|
9a7b4f69ef
|
More tests and some small bugfixes for Z3SmtSolver
Former-commit-id: 71def90649
|
11 years ago |
David_Korzeniewski
|
45bc8ea665
|
Conditional compilation for all parts using z3 by checking STORM_HAVE_Z3
Added first simple tests for Z3SmtSolver and Z3ExpressionAdapter
Former-commit-id: 77ade5ffa6
|
11 years ago |