sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
2408 Commits
2 Branches
0 Tags
187 MiB
Tree: 49dc27077c
Branches Tags
${ item.name }
Create tag ${ searchTerm }
Create branch ${ searchTerm }
from '49dc27077c'
${ noResults }
Commit Graph

195 Commits (49dc27077c2d3e5546456cfb13da65af6015a206)

Author SHA1 Message Date
dehnert f54b5671ea Done refactoring MathSAT expression adapter.
11 years ago
dehnert a061cdbed8 Started refactoring MathSAT adapter.
11 years ago
dehnert 84bfd58884 Minor refactoring of Z3 expression adapter.
11 years ago
dehnert 81571878f7 Further refactoring of MathSAT solver.
11 years ago
dehnert 6eb415f87f Tests for MathSAT now run through on Mac OS.
11 years ago
dehnert d8be64f0d7 Started on making MathSatSmtSolver work properly.
11 years ago
dehnert 90b0f20167 Reachability Rewards can now be computed in parametric DTMCs (modulo bugs)
11 years ago
dehnert b7492d543a Further work regarding rewards in parameterized models. Note: this includes some debug output.
11 years ago
dehnert 3231ea6c06 Moved to new macros.
11 years ago
dehnert 27b630bccc Removed debug output.
11 years ago
dehnert 08959a6a32 Intermediate commit.
11 years ago
dehnert 79798e2cb1 Fixed the reward-issue even harder.
11 years ago
dehnert c4c7794069 Intermediate commit.
11 years ago
dehnert a7bce9e520 Removed debug output and fixed the reward issue a bit more.
11 years ago
dehnert 7cd0dfe8b0 Fixed an issue regarding the reward model generation.
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).
11 years ago
David_Korzeniewski 25d87bae06 Builds fine, still no tests yet
11 years ago
dehnert c2abd9968f Introduced constants comparator in explicit model adapter.
11 years ago
dehnert ff5902a17c Some fixes.
11 years ago
David_Korzeniewski 56edf1e126 Initial MathSat integration.
11 years ago
dehnert 4804ed636d Adapted some code to work with carl.
11 years ago
sjunges d78d88b84d added export of constraints and resultfile
11 years ago
dehnert 385f7b7465 Added option to sort trivial SCC in descending order wrt. to their distances from the initial state. Added some more timing recordings.
11 years ago
dehnert 4eea90646a Fixed attributes of some example files. Added option to eliminate entry states in the very end (added option module for model checking of parametric models). Added feature to specify the formulas to check on the command line.
11 years ago
dehnert 2fa3036dc3 Added functionality to replace identifiers in an expression with the values given in an valuation. State-variables now get replaced in probabilities specified by a parameterized model. Fixed and added some parameterized models.
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.
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.
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).
11 years ago
sjunges 5817fe50b6 post merge fixes
11 years ago
dehnert 9ad12616e2 Renamed files in settings module a bit. Started on the pseudo-modular module-settings.
11 years ago
dehnert 96e1f8faf9 Renamed Settings class to SettingsManager.
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.
11 years ago
dehnert 418ce8b625 Fixed some problems related to the memory-mapped file.
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.
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.
11 years ago
dehnert e2c2177dca Adapted MaxSAT-based minimal command set generator to some recent changes to make it work again.
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.
11 years ago
David_Korzeniewski ee89065b07 Fixed type error on gcc and clang (int_fast64_t is not the same type as on msvc)
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
11 years ago
David_Korzeniewski a0319cb6e7 Model Generation and Tests for translating from z3 to storm
11 years ago
David_Korzeniewski 9a7b4f69ef More tests and some small bugfixes for Z3SmtSolver
11 years ago
David_Korzeniewski 45bc8ea665 Conditional compilation for all parts using z3 by checking STORM_HAVE_Z3
11 years ago
David_Korzeniewski 4e6c9b7d6b Implemented translating z3 expressions to storm expressions
11 years ago
sjunges ccbfef288d removed some debug output
11 years ago
dehnert db232fe39b Moved from pair to MatrixEntry as the basic building block of the matrix. Now matrix elements can be accessed in a more readable way.
11 years ago
David_Korzeniewski 83d2a1c315 Adapted Z3ExpressionAdapter to deletion of constant expressions. Added functionality to autocreate variables in the solver. Added function to get variables and their types from an expression.
11 years ago
David_Korzeniewski 98f87a5e6d Adapted Z3ExpressionAdapter for new expressions
11 years ago
dehnert 5816bd8860 Bugfix for explicit model adapter: empty choice labeling was not created for automatically added self-loops.
11 years ago
sjunges d4c2657856 Parsing parameteric dtmcs and exporting them to smt2
11 years ago
sjunges 7ca6a4edeb sub part for parameters, working parsing for non parametric systems into a parametric system
11 years ago