1175 Commits (219d86ad95ef561ac4475f2c05eb26b07505e806)
 

Author SHA1 Message Date
Dave Parker fbec092ace Check for overflows added to simulator, but disabled for now. 15 years ago
Dave Parker de11a8685e Code tidy. 15 years ago
Dave Parker 3f734e76db Added func in odd to convert index to BDD. 15 years ago
Dave Parker 31707a7729 Two bugs in LTL model checking for MDPs. 15 years ago
Dave Parker b6d4a15737 Simulator disabled for PTAs. 15 years ago
Dave Parker 5666a51b0c Possible bug fix: Termination of simulation check in GUI not detected (thread issue?). 15 years ago
Dave Parker a97d6d9841 Digitsl clocks enabled for model checking in GUI. 15 years ago
Dave Parker c4b176232c Error message when trying to do bounded properties with digital clocks. 15 years ago
Dave Parker c19b257e70 Code tidy. 15 years ago
Dave Parker 146b5f35be Moved digital clocks translation so it can be done per property (in PrismCL). 15 years ago
Dave Parker 3da3b1e298 Bugfix: no double display of error message in GUI result dialog. 15 years ago
Dave Parker dcfc7c59de Added option to do experiments for PTAs in GUI. 15 years ago
Dave Parker 4b3cf8c6b4 Code tidy. 15 years ago
Dave Parker e9545cac7c Added option to verify PTAs in GUI (no experiments yet). 15 years ago
Dave Parker da9ca7124c Small tidy in simpath generation. 15 years ago
Dave Parker 29c462722c Simulator bugfix: exported path was one short. 15 years ago
Dave Parker fcf236acd3 Added (self-loop) deterministic loop detection to simulator. 15 years ago
Dave Parker 55899baab5 Simulator bug: picking wrong random choice in CTMCs with multi-update commands (e.g. DTMCs seen as CTMCs). 15 years ago
Dave Parker 7607a567da Add isDeterministic() method to TransitionList. 15 years ago
Dave Parker 03cf76f5d6 Fix: floor/ceil of NaN/inf is an error. 15 years ago
Dave Parker eeb31a9735 Simulator complains about invalid (-ve/NaN) probs/rates. 15 years ago
Dave Parker d36cb8496a Correct handling of mod (error on non-positive divisor, positive result for negative dividend). 15 years ago
Dave Parker bf16bd754b Correct handling of mod (error on non-positive divisor, positive result for negative dividend) (NB: needs CUDD fix too). 15 years ago
Dave Parker 904b3436b0 Correct detection of erroneous integer powers with negative exponent. 15 years ago
Dave Parker ff697f7196 Correct detection of erroneous integer powers with negative exponent. 15 years ago
Dave Parker 7ac675b050 Added -nobuild switch. 15 years ago
Dave Parker 25b65c4f26 Added -exportprismconst switch. 15 years ago
Dave Parker aba274af88 Removed diagonal-free restriction for digital clocks. 15 years ago
Dave Parker bc834d7d83 Better property checks for PTAs, including new computation of prob operator nesting. Better handling of labels in PTA model checker. 15 years ago
Dave Parker 0070e79fa0 NOTES. 15 years ago
Dave Parker 993035107c PTA notes. 15 years ago
Dave Parker 5c59047e2f Tidy up of PTA examples. 15 years ago
Dave Parker c3626c54b0 Version num. 15 years ago
Dave Parker 801df965c7 Version num. 15 years ago
Dave Parker 40d2cadd45 Tidy PTA examples. 15 years ago
Dave Parker 873791b389 NOTES. 15 years ago
Dave Parker 45c1f3f367 NOTES. 15 years ago
Dave Parker bbaba8bddc Removed examples dir. 15 years ago
Dave Parker 7381c5bd3c NOTES. 15 years ago
Dave Parker 5d8ce238cf Moving bisim/expected parts of PTA MC to prism-pta. 15 years ago
Dave Parker 52e3d712e7 Added -exportadvmdp switch. 15 years ago
Dave Parker d36ac54853 IndexedSet utility method getEntrySet(). 15 years ago
Dave Parker b501caf1f1 Improvements to ConstructModel (explicit). 15 years ago
Dave Parker 48a2e4bcc8 Undo last commit. 15 years ago
Dave Parker ed96947903 Improvements to ConstructModel (explicit). 15 years ago
Dave Parker dc90c17760 Export to PRISM language from explicit models. 15 years ago
Dave Parker 993b33264c Export to PRISM language from explicit models. 15 years ago
Dave Parker 714c51cfb8 NOTES. 15 years ago
Dave Parker f9692fb9a4 Moved examples/pta to prism-examples. 15 years ago
Dave Parker 745794c57a Put PTA files in main examples dir. 15 years ago