s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
2700 Commits
5 Branches
0 Tags
31 MiB
Tree: ff49cfd2a6
Branches Tags
${ item.name }
Create tag ${ searchTerm }
Create branch ${ searchTerm }
from 'ff49cfd2a6'
${ noResults }
Commit Graph

2700 Commits (ff49cfd2a6a73697fe83e276e2f2999e434ac5af)
 

Author SHA1 Message Date
Dave Parker 5b8f3cd4d6 Add iterator to get actions from a DTMC (not usually stored, yet), defaulting them to null, and display these from exportToPrismExplicitTra().
11 years ago
Dave Parker d0f3e91387 Some code tidying (automatic mostly) for merging purposes.
11 years ago
Dave Parker 7eef2a266c Fix a few compiler warnings.
11 years ago
Dave Parker 5238c76c4c Optimisation in the simulator for models with very large numbers of actions (from Marcus Daum + Joachim Klein).
11 years ago
Dave Parker be12b376dc Bug fix in double_vector_to_dist (dv.cc) - did not bail out when there are too many distinct values due to overflow of short int counter. [found by Chris Dehnert]
11 years ago
Dave Parker 28cf06cd57 prism-auto: Revert -e/--echo switch to old behaviour and add --echo-full for extended functionality from Joachim Klein.
11 years ago
Dave Parker f7f7e736d2 prism-auto: Fix some bugs and document more of the functions.
11 years ago
Dave Parker 835e95a861 Don't print optimal strategy to screen when exporting it (explicit engine).
11 years ago
Dave Parker 683f714edf Small fix in LTSFromDA: successors might not be unique (spotted by Joachim Klein).
11 years ago
Dave Parker f19cb029d7 Parse modifiers on R and S operators as well as P.
11 years ago
Dave Parker 7f1315dfc1 Do not allow any ExpressionQuant modifiers for now.
11 years ago
Dave Parker 8475ae29be ExpressionQuant: mode -> modifier.
11 years ago
Dave Parker adba5a090c ExpressionQuant: mode -> modifier.
11 years ago
Dave Parker 1945ef1d40 More refactoring of ExpressionQuant and add "mode" field, currently ignored.
11 years ago
Dave Parker 5c8439c0e6 Convert ExpressionQuant from interface to abstract class and push some shared code in ExpressionProb/Reward/SS into it.
11 years ago
Dave Parker 86c3e3e3cc New default for CUDD max memory (1GB) and more flexible usage of that setting: allow memory in format 125k, 50m, 4g, etc.
11 years ago
Dave Parker b4f05f3cd0 Add possibility to specify type to -exportpropaut switch (dot or txt), e.g. -exportpropaut:dot dra.dot.
11 years ago
Dave Parker 37b4284bfd DA can print to a PrismLog in either text or Dot format.
11 years ago
Dave Parker 8454511dad DA can print to a PrintStream or a PrismLog.
11 years ago
Dave Parker d2c08418db Add another simplification of DRAs - remove any state in a K_i set that does not occur in a non-trivial SCC of the DRA. This also allows more DRAs to be simplified to DFAs.
11 years ago
Dave Parker c17f92e172 Add LTS model type and expose underlying graph of a DA as an LTS.
11 years ago
Dave Parker e9afcf0419 Add default implementation of infoString() and infoStringTable() to ModelExplicit.
11 years ago
Dave Parker be834a8aff Align explicit SCComputer with symbolic one - it should not include trivial SCCs in the set computed; these should be stored separately.
11 years ago
Dave Parker a948079456 Fix comments in prism.SCCComputer to clarify that it computes non-trivial SCCs.
11 years ago
Dave Parker 98dcb3c803 Code tidy
11 years ago
Dave Parker 3fa59734a9 More use of PrismNotSupportedException.
11 years ago
Dave Parker 7352ad17b3 Small optimisation in LTL model checking: reduce number of propositions used in deterministic automaton by checking for negations.
11 years ago
Dave Parker f1d6d850ce Fix in prism-auto
11 years ago
Dave Parker b12953b937 Make use of the new PrismNotSupportedException.
11 years ago
Dave Parker 88928e8b89 New PrismNotSupportedException, to be throw when a model/prop/engine combination is not supported. Displays as UNSUPPORTED, not FAIL, in test mode. [from Joachim Klein]
11 years ago
Dave Parker fb7208d792 Improved "echo" (-e) functionality for prism-auto: displays more accurately what prism-auto would do, including test (-t) and log (-l) modes [from Joachim Klein].
11 years ago
Dave Parker c0cd3810f2 prism-auto bugfix: something got broken for processing property files during recent refactoring.
11 years ago
Dave Parker 87ad5c37b7 Remove typo.
11 years ago
Dave Parker 523d73a8ea Set locale for display of numerical values - otherwise, e.g. with LANG=de_DE.UTF-8, probabilities will be exported in the form 0,5 not 0.5 (reported by Joacim Klein).
11 years ago
Dave Parker 30c5001aaf Increase the default Java max memory (from to 512m to 2g) - should be ok these days.
11 years ago
Dave Parker c1681a04b2 Increase the default Java stack size - was consistently crashing on Tarjan SCC detection on a non-huge model (as reported by Steffen Marcker).
11 years ago
Dave Parker 8b062cf410 prism-auto can take multiple files/dirs as arguments.
11 years ago
Dave Parker 640101bdcc Improved detection of export files detected by prism-auto.
11 years ago
Dave Parker aa65fa1ea3 Fix documentation (-help xxx) about -exportmodel and -importmodel.
11 years ago
Dave Parker 079e9ea36a Typos.
11 years ago
Dave Parker 3c17f39e18 prism-auto: Remove debug output.
11 years ago
Dave Parker 46e7e979e8 prism-auto: Some improvements in detection of export files.
11 years ago
Dave Parker 3ca0c4fb81 prism-auto: Print error if file/dir does not exist
11 years ago
Dave Parker df7198f06e Comment
11 years ago
Dave Parker 2e2639d38d prism-auto debug output.
11 years ago
Dave Parker c561f38c75 Unbreak prism-auto (after previous refactoring).
11 years ago
Dave Parker 3d6976f094 Fix in prism-auto: need to read model args files too when running a .test file.
11 years ago
Dave Parker c3bd656cc7 Fix in prism-auto: do not rename export files unless in test mode.
11 years ago
Dave Parker 79eda01716 Fix in prism-auto: do not look for matching export files unless we need to.
11 years ago
Dave Parker cfb871b92b Fix in prism-auto: model files should be treated the same whether specified directly or found in a directory. Also some refactoring.
11 years ago