{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":250513297,"defaultBranch":"robots","name":"prism","ownerLogin":"ori-goals","currentUserCanPush":false,"isFork":true,"isEmpty":false,"createdAt":"2020-03-27T11:10:41.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/43650988?v=4","public":true,"private":false,"isOrgOwned":true},"refInfo":{"name":"","listCacheKey":"v0:1726780581.0","currentOid":""},"activityList":{"items":[{"before":"61af6642161bed370d712d7b77a05f3753a231aa","after":null,"ref":"refs/heads/robots-fixes","pushedAt":"2024-09-19T21:16:21.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"davexparker","name":"Dave Parker","path":"/davexparker","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/6075003?s=80&v=4"}},{"before":"52f37eebf3a8ffe5f891464e7384be79e2b515fe","after":"a7c57b9fe33d679e0e52f6ebd335ac6df2cdd8f1","ref":"refs/heads/imp/explicit-models","pushedAt":"2024-09-17T10:31:41.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"heuristicus","name":"Michal Staniaszek","path":"/heuristicus","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/636456?s=80&v=4"},"commit":{"message":"explicit loading: use the new transition reward loading, lists are null if no file is received","shortMessageHtmlLink":"explicit loading: use the new transition reward loading, lists are nu…"}},{"before":"2eef6f0ee44700d94e98b896e83967b1d503dd38","after":"11f14512cc2ba126f28c671c25bb5bfebaeb8754","ref":"refs/heads/robots","pushedAt":"2024-09-17T10:24:03.000Z","pushType":"pr_merge","commitsCount":3,"pusher":{"login":"heuristicus","name":"Michal Staniaszek","path":"/heuristicus","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/636456?s=80&v=4"},"commit":{"message":"Merge pull request #9 from ori-goals/robots-fixes\n\nCompile fixes for PRISM master","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2530731683\" data-permission-text=\"Title is private\" data-url=\"https://github.com/ori-goals/prism/issues/9\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/ori-goals/prism/pull/9/hovercard\" href=\"https://github.com/ori-goals/prism/pull/9\">#9</a> from ori-goals/robots-fixes"}},{"before":null,"after":"61af6642161bed370d712d7b77a05f3753a231aa","ref":"refs/heads/robots-fixes","pushedAt":"2024-09-17T10:17:23.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"heuristicus","name":"Michal Staniaszek","path":"/heuristicus","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/636456?s=80&v=4"},"commit":{"message":"More compile fixes for latest PRISM master (reward storage).","shortMessageHtmlLink":"More compile fixes for latest PRISM master (reward storage)."}},{"before":"b6d502ed9de4202dd0b879d768c9f98f5c405a6c","after":null,"ref":"refs/heads/robots-fixes","pushedAt":"2024-09-17T10:12:53.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"heuristicus","name":"Michal Staniaszek","path":"/heuristicus","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/636456?s=80&v=4"}},{"before":null,"after":"b6d502ed9de4202dd0b879d768c9f98f5c405a6c","ref":"refs/heads/robots-fixes","pushedAt":"2024-09-17T10:11:20.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"heuristicus","name":"Michal Staniaszek","path":"/heuristicus","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/636456?s=80&v=4"},"commit":{"message":"More compile fixes for latest PRISM master (reward storage).","shortMessageHtmlLink":"More compile fixes for latest PRISM master (reward storage)."}},{"before":"429c63006dd7be8138a27a17c64ff84884f0b9f5","after":"2eef6f0ee44700d94e98b896e83967b1d503dd38","ref":"refs/heads/robots","pushedAt":"2024-09-17T08:43:43.000Z","pushType":"push","commitsCount":76,"pusher":{"login":"heuristicus","name":"Michal Staniaszek","path":"/heuristicus","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/636456?s=80&v=4"},"commit":{"message":"Merge remote-tracking branch 'upstream/master' into robots","shortMessageHtmlLink":"Merge remote-tracking branch 'upstream/master' into robots"}},{"before":"7c920e06fe22266093007f400f40f71190ff5d6e","after":"429c63006dd7be8138a27a17c64ff84884f0b9f5","ref":"refs/heads/robots","pushedAt":"2024-09-17T08:40:12.000Z","pushType":"push","commitsCount":249,"pusher":{"login":"heuristicus","name":"Michal Staniaszek","path":"/heuristicus","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/636456?s=80&v=4"},"commit":{"message":"dont tell prism to export strat using new stuff in case of multi or Rmax - still not supported on the prism side","shortMessageHtmlLink":"dont tell prism to export strat using new stuff in case of multi or R…"}},{"before":"e8eb0c71f9300808a53017e26c034ac61021f9fb","after":"7c920e06fe22266093007f400f40f71190ff5d6e","ref":"refs/heads/robots","pushedAt":"2024-09-17T08:40:06.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"heuristicus","name":"Michal Staniaszek","path":"/heuristicus","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/636456?s=80&v=4"},"commit":{"message":"add functionality for transient analysis","shortMessageHtmlLink":"add functionality for transient analysis"}},{"before":"4974cb2688cb3cf9f4b8022c4681c48d0edf9686","after":"52f37eebf3a8ffe5f891464e7384be79e2b515fe","ref":"refs/heads/imp/explicit-models","pushedAt":"2024-09-16T14:36:34.000Z","pushType":"push","commitsCount":78,"pusher":{"login":"heuristicus","name":"Michal Staniaszek","path":"/heuristicus","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/636456?s=80&v=4"},"commit":{"message":"Merge branch 'robots' into imp/explicit-models","shortMessageHtmlLink":"Merge branch 'robots' into imp/explicit-models"}},{"before":"6112a5be83dc5d6d4852706283ee7f932215c54e","after":"4974cb2688cb3cf9f4b8022c4681c48d0edf9686","ref":"refs/heads/imp/explicit-models","pushedAt":"2024-09-16T14:29:54.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"heuristicus","name":"Michal Staniaszek","path":"/heuristicus","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/636456?s=80&v=4"},"commit":{"message":"explicit loading: use the new transition reward loading, lists are null if no file is received","shortMessageHtmlLink":"explicit loading: use the new transition reward loading, lists are nu…"}},{"before":"b3f207fda1ff3dc2e05ad7382db3f4371239a8f2","after":"6112a5be83dc5d6d4852706283ee7f932215c54e","ref":"refs/heads/imp/explicit-models","pushedAt":"2024-09-16T14:13:21.000Z","pushType":"push","commitsCount":251,"pusher":{"login":"heuristicus","name":"Michal Staniaszek","path":"/heuristicus","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/636456?s=80&v=4"},"commit":{"message":"Merge branch 'robots' into imp/explicit-models","shortMessageHtmlLink":"Merge branch 'robots' into imp/explicit-models"}},{"before":"c4adffa629de0c84c05a3118c49daa2c70e8607a","after":"e8eb0c71f9300808a53017e26c034ac61021f9fb","ref":"refs/heads/robots","pushedAt":"2024-09-16T14:11:59.000Z","pushType":"pr_merge","commitsCount":77,"pusher":{"login":"heuristicus","name":"Michal Staniaszek","path":"/heuristicus","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/636456?s=80&v=4"},"commit":{"message":"Merge pull request #7 from ori-goals/upstream-update\n\nUpdate to latest upstream","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2528600863\" data-permission-text=\"Title is private\" data-url=\"https://github.com/ori-goals/prism/issues/7\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/ori-goals/prism/pull/7/hovercard\" href=\"https://github.com/ori-goals/prism/pull/7\">#7</a> from ori-goals/upstream-update"}},{"before":null,"after":"b326f16ef068159b11eeee570499505dec757333","ref":"refs/heads/upstream-update","pushedAt":"2024-09-16T14:10:57.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"heuristicus","name":"Michal Staniaszek","path":"/heuristicus","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/636456?s=80&v=4"},"commit":{"message":"Merge remote-tracking branch 'upstream/master' into upstream-update","shortMessageHtmlLink":"Merge remote-tracking branch 'upstream/master' into upstream-update"}},{"before":"c35a9b07627f7b6e37492b95275af4b5fc8fdffe","after":"c4adffa629de0c84c05a3118c49daa2c70e8607a","ref":"refs/heads/robots","pushedAt":"2024-09-16T14:09:04.000Z","pushType":"pr_merge","commitsCount":250,"pusher":{"login":"heuristicus","name":"Michal Staniaszek","path":"/heuristicus","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/636456?s=80&v=4"},"commit":{"message":"Merge pull request #6 from ori-goals/robots2\n\nTry merging robots2 again, previous merge was squash","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2528509548\" data-permission-text=\"Title is private\" data-url=\"https://github.com/ori-goals/prism/issues/6\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/ori-goals/prism/pull/6/hovercard\" href=\"https://github.com/ori-goals/prism/pull/6\">#6</a> from ori-goals/robots2"}},{"before":"ffff48fab5c5bfc6648fb9e59f5926702bcd032c","after":"429c63006dd7be8138a27a17c64ff84884f0b9f5","ref":"refs/heads/robots2","pushedAt":"2024-09-16T14:08:36.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"heuristicus","name":"Michal Staniaszek","path":"/heuristicus","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/636456?s=80&v=4"},"commit":{"message":"dont tell prism to export strat using new stuff in case of multi or Rmax - still not supported on the prism side","shortMessageHtmlLink":"dont tell prism to export strat using new stuff in case of multi or R…"}},{"before":"429c63006dd7be8138a27a17c64ff84884f0b9f5","after":"ffff48fab5c5bfc6648fb9e59f5926702bcd032c","ref":"refs/heads/robots2","pushedAt":"2024-09-16T13:31:40.000Z","pushType":"push","commitsCount":76,"pusher":{"login":"heuristicus","name":"Michal Staniaszek","path":"/heuristicus","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/636456?s=80&v=4"},"commit":{"message":"Merge remote-tracking branch 'upstream/master' into robots2","shortMessageHtmlLink":"Merge remote-tracking branch 'upstream/master' into robots2"}},{"before":null,"after":"429c63006dd7be8138a27a17c64ff84884f0b9f5","ref":"refs/heads/robots2","pushedAt":"2024-09-16T13:15:50.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"heuristicus","name":"Michal Staniaszek","path":"/heuristicus","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/636456?s=80&v=4"},"commit":{"message":"dont tell prism to export strat using new stuff in case of multi or Rmax - still not supported on the prism side","shortMessageHtmlLink":"dont tell prism to export strat using new stuff in case of multi or R…"}},{"before":"e018a8c511dbeb4aef4aec8a6a609d1c9acf77ac","after":"b3f207fda1ff3dc2e05ad7382db3f4371239a8f2","ref":"refs/heads/imp/explicit-models","pushedAt":"2024-09-09T12:36:21.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"heuristicus","name":"Michal Staniaszek","path":"/heuristicus","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/636456?s=80&v=4"},"commit":{"message":"rapport talker: avoid using current model when parsing properties, prevents crash when loading explicit models","shortMessageHtmlLink":"rapport talker: avoid using current model when parsing properties, pr…"}},{"before":"26931c49b8e8e3e33e449fd04c8f86ee69d8c247","after":"e018a8c511dbeb4aef4aec8a6a609d1c9acf77ac","ref":"refs/heads/imp/explicit-models","pushedAt":"2024-09-09T09:37:59.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"heuristicus","name":"Michal Staniaszek","path":"/heuristicus","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/636456?s=80&v=4"},"commit":{"message":"rapport talker: only add explicit label/reward files if they exist","shortMessageHtmlLink":"rapport talker: only add explicit label/reward files if they exist"}},{"before":null,"after":"26931c49b8e8e3e33e449fd04c8f86ee69d8c247","ref":"refs/heads/imp/explicit-models","pushedAt":"2024-07-29T10:59:32.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"heuristicus","name":"Michal Staniaszek","path":"/heuristicus","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/636456?s=80&v=4"},"commit":{"message":"can load models from explicit files by passing explicit_model following the command","shortMessageHtmlLink":"can load models from explicit files by passing explicit_model followi…"}},{"before":"429c63006dd7be8138a27a17c64ff84884f0b9f5","after":null,"ref":"refs/heads/robots2","pushedAt":"2024-06-27T15:18:57.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"bfalacerda","name":"Bruno Lacerda","path":"/bfalacerda","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4320588?s=80&v=4"}},{"before":"7c920e06fe22266093007f400f40f71190ff5d6e","after":"c35a9b07627f7b6e37492b95275af4b5fc8fdffe","ref":"refs/heads/robots","pushedAt":"2024-06-27T15:18:51.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"bfalacerda","name":"Bruno Lacerda","path":"/bfalacerda","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4320588?s=80&v=4"},"commit":{"message":"Robots2 (#4)\n\nMany updates from prism main repo and edits to make robots stuff work:\r\n\r\n* GUI fix: better remembering of previous model constants.\r\n\r\nUse values stored in Prism rather than caching locally.\r\nAlso make GUI simulator default to previous constants too.\r\n\r\n* README contact details update.\r\n\r\n* Implement test for short-circuit evaluation\r\n\r\n* Fix short-circuit evaluation for expressions\r\n\r\n* Add ModelGenerator.getChoiceIndexByAction(), with default implementation.\r\n\r\n* DistributionOver class for discrete distributions, plus sample() methods.\r\n\r\n* Update and re-design of classes to store strategies.\r\n\r\nStrategy interface:\r\n\r\n- main purpose clarified: represents a strategy with respect to a specific,\r\n  constructed model and, by default, defines choices by action (as an Object)\r\n- can also provide getChoiceIndex() but this is not to be relied upon\r\n  (mainly because model choice ordering varies across engines)\r\n- by default, queries take both s (state index) and m (memory index);\r\n  the interface (formerly subclass) MDStrategy (memoryless deterministic)\r\n  adds methods that just take the state index s\r\n- getNumStates() method moved to this interface\r\n- strategies can implement whyUndefined() to explain missing choices\r\n- other utility methods: isChoiceDefined(), getChoiceActionString()\r\n- new methods for info about memory:  getInitialMemory(), getUpdatedMemory()\r\n- \"interactive\" methods, which track the current state of the strategy\r\n  (i.e., initialise, update) are removed\r\n- implementations (MDStrategy*) are updated accordingly\r\n- new subclass StrategyExplicit added for implementations of Strategy\r\n  attached to explicit engine models\r\n\r\nStrategyGenerator: new interface supporting provision of interfaces\r\nat the State (not state index) level, and in an interactive fashion\r\n(states are supplied sequentially and the strategy keeps track of its\r\ncurrent state, memory, etc.). Not yet used.\r\n\r\nStrategyInfo: common super-interface for Strategy and StrategyGenerator\r\nsupplying basic info (e.g., class of strategy)\r\n\r\nStrategyWithStates: base class for implementations of Strategy, which\r\nimplements the StrategyGenerator interface, given a state-to-index\r\nlook-up mechanism.\r\n\r\nSupport for randomised strategies also added:\r\n\r\n- for randomised strategies, getActionChoice() returns an instance of\r\n  DistributionOver<Object> rather than just Object\r\n- for convenience, Strategy has getChoiceActionProbability(), isActionChosen()\r\n  and sampleChoiceAction(); StrategyGenerator has comparable methods\r\n  getCurrentChoiceActionProbability(), isActionChosenCurrently()\r\n  and sampleCurrentChoiceAction()\r\n- both have default implementations based on utility methods\r\n  included within StrategyInfo\r\n\r\n* Proper support for SimulatorEngine following a strategy.\r\n\r\nprism.Prism now retains a Strategy if generated/returned during model checking,\r\naccessible via getStrategy(). There is a new method loadStrategyIntoSimulator()\r\nto pass the current strategy to the simulator.\r\n\r\nSimulatorEngine has a new mechanism for loading a strategy, as a StrategyGenerator,\r\nwhich takes care of providing a strategy and mapping it to the State view of a model.\r\nIt is also optional whether it is enforced or not, during automatic path  generation,\r\nvia method ​setStrategyEnforced(). The state/decision of the strategy can  be queried\r\nfor the current state: isTransitionEnabledByStrategy(), getStrategyDecisionString().\r\n\r\nPath classes (optionally) store strategy info (current decision and memory) in states.\r\n\r\n* Add GUI support for generating strategies and viewing/enforcing them in the simulator.\r\n\r\n* Add GUI support for export of current strategy (actions, induced model, dot).\r\n\r\n* GUI: Add \"Strategies\" menu at top-level.\r\n\r\n* Construction of product of (explicit engine) model and strategy.\r\n\r\n* Strategy synthesis (finite-memory) for MDP bounded reachability (explicit engine).\r\n\r\n* Strategy synthesis (finite-memory) for LTL on MDPs (explicit engine).\r\n\r\n* Fix for GUI strategy handling (cleanly ignore when unusable).\r\n\r\n* Create BigIntegers properly in BigRational\r\n\r\n- Create BigIntegers from int/long directly without String conversion\r\n- Use BigInteger#valueOf instead of invoking constructor directly\r\n\r\n* Use BigInteger#abs to compute absolute value\r\n\r\n* Add option to export model and props labels to same file\r\n\r\nBoth -exportmodel and -exportlabels have an option to export\r\nlabels from a model and properties file to the same file.\r\nThe default behaviour only exports labels defined in the model.\r\n\r\nNote: This changes the default from the previous version which\r\nalways exported labels from a properties file if present.\r\n\r\nFixes #179\r\n\r\n* Adapt tests to new label export behaviour\r\n\r\n* Add -exportproplabels to export (just) properties file labels to a file.\r\n\r\n* Test -exportproplabels\r\n\r\n* Adapt GUI commands for label export\r\n\r\n* Improve constructors of StateRewardsArray\r\n\r\n* Fix short-circuiting for ? (if-then-else) in expression evaluation.\r\n\r\nAs done recently for & and | in 5bdee58d.\r\n\r\nAnd as less recently broken in d1678111.\r\n\r\n* Add subset-only variants of apply methods to explicit.StateValues.\r\n\r\n* Implement short-circuiting of &,|,=>,? during (explicit) model checking.\r\n\r\nAs raised in #211.\r\n\r\nAnd generally make more use of statesOfInterest in explicit engine\r\nmodel checking. In particular: respect this for operators handled\r\nby passing to apply methods within StateValues.\r\n\r\n* Some tests for short-circuiting.\r\n\r\n* Update CHANGELOG.\r\n\r\n* prism-auto Python compatibility fix (no list.copy() in 2.x or <3.3).\r\n\r\nFixes #215\r\n\r\n* Cleaner handling of failures during reward export.\r\n\r\nSpecifically: if unsupported (notably explicit engine transition\r\nrewards), an empty rewards file is not erroneously created.\r\n\r\n* Small tweak in model export precision setting.\r\n\r\n* Import of multiple reward structures + optional header (explicit).\r\n\r\nExplicit-engine import of rewards from files now supports multiple\r\nreward structures across several files, as already done for export.\r\n\r\nExplicit files for import/export of state rewards can optionally\r\ninclude a #-commented header giving the reward structure name (if\r\npresent) and the type of rewards (state or transition), e.g.:\r\n\r\n# Reward structure: \"r\"\r\n# State rewards\r\n\r\nExplicit engine now supports import/export of files with headers.\r\n\r\nNeither multiple reward import or header generation are yet\r\nenabled in PRISM itself.\r\n\r\nExplicitFilesRewardGenerator is refactored, making it an abstract\r\nclass, and ExplicitFilesRewardGenerator4Explicit is added, to allow\r\nlater re-use of the code by the symbolic engine.\r\n\r\n* Import of multiple reward structures + optional header (symbolic).\r\n\r\nImplementation for symbolic engines of functionality in previous commit.\r\n\r\n* Import of multiple reward structures + reward file headers.\r\n\r\nSupport for importing multiple rewards from separate files added.\r\nFrom the command-line, this can be achieved using multiple\r\n-importstaterewards switches. Alternatively, the -importmodel switch,\r\nif prompted to import a .srew file (either via .all or by including\r\n.srew in the list of file extensions), looks for indexed versions\r\n(1.srew, etc.), as generated by -exportmodel.\r\n\r\nHeaders (name/type) now added to exported state reward files by default.\r\nThis can be disabled from the command-line by using -noexportheaders\r\nor using the \"Include headers in model exports\" option from the GUI.\r\n\r\nVarious regression tests are added/modified.\r\n\r\n* Add header comments to (symbolically) exported transition reward files too.\r\n\r\n* Adapt reward export header format.\r\n\r\nThe new format is (e.g., for state rewards):\r\n\r\n# Reward structure \"name\"\r\n# State rewards\r\n\r\nor:\r\n\r\n# Reward structure\r\n# State rewards\r\n\r\nfor unnamed reward structures.\r\n\r\n* Error message typo.\r\n\r\n* Implement clone(), i.e. shallow copy, for ASTElement classes.\r\n\r\n* Refactor ASTElement deepCopy() to use clone().\r\n\r\nPreliminary refactoring of ASTElement.deepCopy() into two steps,\r\nthe first using clone(). See the next commit for details.\r\n\r\n* Refactor ASTElement deepCopy() into clone() and DeepCopy visitor.\r\n\r\nThis commit (combined with the previous two) separates deep-copying\r\nof an AST element into two steps:\r\n\r\n1. Creating a shallow copy of the AST node\r\n2. Recursively cloning the fields and child nodes using a visitor DeepCopy\r\n\r\nThis enables the programmer to create both shallow copies (aka clones in\r\nJava terminology) and deep copies. The visitor DeepCopy provides a hook\r\ninto the copying process. This can be useful, e.g., to modify the copy on\r\nthe fly or cache copied elements. It also provides a cleaner interface\r\nsince traversal and copying logic is better separated.\r\n\r\nTo simplify copying child nodes, DeepCopy provides the utility methods\r\n\r\nTo adapt existing and new subclasses of ASTElement:\r\n\r\n1. Override #clone such that (a) the type of the callee is returned and\r\n   (b) all collection fields are cloned too. See Command#clone() and\r\n   ConstantList#clone for examples.\r\n\r\n2. Override the abstract method #deepCopy(DeepCopy) such that it (a)\r\n   returns the type of the callee and (b) deep copies its child nodes\r\n   and fields using the utility methods of the provided visitor. See\r\n   Command#deepCopy and ConstantList#deepCopy for examples. These\r\n   methods are shorter and cleaner than the old #deepCopy method.\r\n\r\nCloses #217.\r\n\r\n* ASTElement refactoring: Change all Vectors to Lists and ArrayLists.\r\n\r\n* Align stochastic game classes with PRISM-games.\r\n\r\n* Bug fix in new symbolic model import code when there are no rewards files.\r\n\r\nAlso fixes a surplus DD reference.\r\n\r\n* API change/fix: loadModelFromExplicitFiles needs rewards file _list_.\r\n\r\nAttempt to retain old method with just one File fails, becase the\r\nmethods are ambiguous in the common case where null is passed.\r\n\r\nUse Collections.singletonList(stateRewardsFile) when there is only one.\r\n\r\nAlso fix a bug so that loadModelFromExplicitFiles can be passed null\r\n(that was currently never happening anyway when called from PrismCL).\r\n\r\n* Make ModelGenerator generic: probabilities/rates can be any type.\r\n\r\nClasses that implement this interface using the normal double type\r\nshould still work with minimal changes, namely changing some methods\r\nreturn types from double to Double, e.g. getTransitionProbability.\r\nIdeally they should also specify \"implements ModelGenerator<Double>\"\r\ninstead of \"implements ModelGenerator\", but this is not essential.\r\n\r\nA few methods that require evaluation/calculation of probabilities\r\n(getChoiceProbabilitySum, getProbabilitySum, isDeterministic) now have\r\na default implementation designed to work with generic types.\r\nThis will work out of the box for doubles, but maybe with a slight\r\nperformance hit. So classes implementing ModelGenerator may wish to\r\nimplement these directly if performance is critical.\r\n\r\nCode that uses a ModelGenerator for model exploration or construction\r\nwill likely need to now specify that it assumes ModelGenerator<Double>,\r\nsince getTransitionProbability etc. no longer always returns doubles.\r\n\r\nA new Evaluator class is added to perfom operations on the Value type\r\nused to specify probabilities etc. This approach is intended to allow\r\nexisting types (Double, BigRational, Function) to be used for for\r\ngeneric models without the need for creating additional wrappers around\r\nthem to implement the interface of methods needed here.\r\n\r\n* Make RewardGenerator generic: rewards can be any type.\r\n\r\nClasses that implement this interface using the normal double type\r\nshould still work with minimal changes, namely changing some methods\r\nreturn types from double to Double, e.g. getStateReward.\r\nIdeally they should also specify \"implements RewardGenerator<Double>\"\r\ninstead of \"implements RewardGenerator\", but this is not essential.\r\n\r\nIn a related change, default method implementations in RewardGenerator\r\nnow throw an exception if a reward should be defined but is not,\r\ne.g., if the number of reward structures has been specified to be >0.\r\nPreviously, they returned a default of 0.0, which is no longer suitable\r\nfor any reward type (and probably not sensible anyway).\r\n\r\n* Make ModulesFileModelGenerator and associated classes generic.\r\n\r\nThe \"associated classes\" are Updater, TransitionList, Choice\r\nand ChoiceListFlexi.\r\n\r\nThis is inline with the previous conversion of ModelGenerator to generic form.\r\nAs there, existing use of ModulesFileModelGenerator should be largely\r\nunaffected, since it is set up to work using doubles by default.\r\nIn particular, the existing constructors continue to work. However,\r\nfor compatibility going forward, it is preferable to now use the static\r\nModulesFileModelGenerator.create(...) method instead.\r\n\r\nIn another related change, the check that distributions sum to 1\r\nwhen constructing models with the explicit engine now uses the method\r\nPrismUtils.doublesAreEqual, which is what is implemented in the default\r\nEvaluator for doubles. This uses relative error with epsilon = 1e-12,\r\nwhich is a tighter check than before, but should be fine to allow\r\nthe check to function in the presence of round-off errors.\r\nThis also means that PRISM_SUM_ROUND_OFF from PrismSettings is\r\nnow ignored by the explicit engine.\r\n\r\n* Replace ModulesFileModelGeneratorSymbolic with generic version.\r\n\r\nModulesFileModelGeneratorSymbolic is used for building models for\r\nthe parametric model checking engine. Its now replaced with instances\r\nof ModulesFileModelGenerator<Function>, using the new generic classes.\r\n\r\nVarious classes in the param package, which heavily overlapped with\r\nthe corresponding classes in the simulator package are now removed:\r\nChoiceListFlexi, TransitionList, SymbolicEngine, ModelGeneratorSymbolic.\r\n\r\nIn some related re-arranging, conversion of PRISM expressions to\r\n(parametric) Function objects is moved into FunctionFactory from\r\nModelBuilder (which will eventually be replaced by ConstructModel).\r\nLookups in ConstantLists, previously done there, are now done in\r\nModulesFileModelGenerator, where the rest of constant replacement is.\r\n\r\nCode to compute choice probability sums and normalise is also\r\nremoved from ModelBuilder since this is now handled in the\r\nModulesFileModelGeneratorSymbolic class, in the same fashion as\r\nfor non-parametric models.\r\n\r\n* Add create methods to ModulesFileModelGenerator and use instead of constructors.\r\n\r\n* Convert explicit engine model and reward classes to generic types.\r\n\r\nAll classes and interfaces for models and rewards in the explicit engine\r\nare now generic, with the type variable (Value) denoting the type used\r\nto represent probabilities/rewards/etc. All model classes have a\r\ncorresponding Evaluator attached, which can be used to perform\r\noperations on that type. This is available via the method\r\ngetEvaluator(). For example, getEvaluator().isZero(x) can be used to\r\ncheck if Value x is zero,\r\n\r\nA default implementation of getEvaluator() in the top-level interface\r\nModel creates a fresh Evaluator for doubles to simplify usage in this\r\ncommon case. The base class ModelExplicit provides storage for a custom\r\nEvaluator which can be set with setEvaluator(). This is also initialised\r\nto a fresh Evaluator for doubles by default. The same approach is taken\r\nin the Rewards interface, and a new RewardsExplicit superclass is added\r\nto allow an Evaluator to be stored. The Distribution class, used by some\r\nmodels, is also now generic and also stores a reference to an Evaluator.\r\nSimilarly, the Strategy interfaces are generic, because they may need\r\nto return probabilities if they are randomised.\r\n\r\nMost model classes and most of their methods are now converted to use\r\nthe generic type variable instead of doubles. One exception is methods\r\nsuch as mvMult (multiplication with a vector of doubles), used e.g. in\r\nvalue iteration and other numerical methods. These continue to assume\r\nthe use of doubles. The DTMCSparse and MDPSparse classes also only work\r\nwith doubles. MDPGeneric is now redundant and has been removed.\r\n\r\nVarious bits of functionality that manipulate models have also been\r\nconverted to use the generic type variable instead of doubles. Most\r\nnotably, this includes explicit state model construction\r\n(ConstructModel). Passing a ModelGenerator<Value> yields a Model<Value>,\r\nwhere, as usual, the type of Model depends on the type specified in the\r\nModelGenerator. Construction of rewards (ConstructRewards) is also\r\nsupported. Currently, neither of these are actually connected to code\r\nthat uses anything apart from doubles.\r\n\r\nVarious other pieces of code have been converted, such as: export of\r\nstate rewards to a file (in ProbModelChecker), LTL product construction\r\n(in LTLModelChecker) and bisimulation minimisation (in Bisimulation).\r\nSome code still assumes the use of doubles, most notably the model\r\nchecker classes DTMCModelChecker, MDPModelChecker, etc.. These have been\r\nrewritten (Model -> Model<Double>) to emphasise this, even though this\r\nis mostly only required to fix compiler warnings not errors. Other code\r\nthat does not need to know the Value for a model has also mostly been\r\ntidied up, e.g., Model -> Model<?> and new Model() -> new Model<>(), to\r\nremove compiler warnings.\r\n\r\n* Remove (now unused) sumRoundOff field from simulator.Updater.\r\n\r\nIn recent commits, the check that distributions sum to 1\r\nmoved away from using this field, taken from the PRISM setting.\r\n\r\n* Make symbolic/explicit engines consistent in checking distributions sum to 1.\r\n\r\nIn line with recent changes in the explicit engine, the symbolic model construction\r\nnow uses PrismUtils.doublesAreEqual, which uses relative error with epsilon = 1e-12,\r\nrather than a configurable epsilon value from the PRISM settings.\r\n\r\n* Compile fixes for generic code on POMDPs.\r\n\r\n* Some new methods in EvaluateContext.\r\n\r\n* Remove calls to evaluateExact and castFromBigRational methods.\r\n\r\nThese are generally replaced with a call to the new evaluate()\r\nmethod, passing an EvaluateContext with the appropriate EvalMode.\r\nSometimes a call to castValueTo() is also used.\r\n\r\nRelatedly, for convenience, prism.Evaluator now has an\r\nevalMode() method returning the appropriate EvalMode.\r\n\r\nAll calls to castFromBigRational are gone and it is removed from Type.\r\n\r\nThe only remaining calls to evaluateExact are in the param engine.\r\n\r\n* Simplify \"set constants\" methods in ConstantsList: just take EvaluateContext.\r\n\r\nThis allows the code to evaluate all constants to be simplified too.\r\n\r\n* ModulesFile and PropertiesFile use EvaluateContext for setting/storing constants.\r\n\r\nThe preferred setSomeUndefinedConstants() method, to set constants, now takes an\r\nEvaluateContext. The EvaluateContext is available via getUndefinedEvaluateContext(),\r\nsimilar to before. The old set methods still work, but are deprecated.\r\n\r\nLocally, we also store the evaluated values for _all_ constants in an\r\nEvaluateContext. More importantly, this also retains the evaluation mode.\r\nThis firms up the expected usage of ModulesFile and PropertiesFile in that\r\nsetSomeUndefinedConstants() specifies both the necessary constant values\r\nand the evaluation mode, and that these remain the same until called again.\r\nThey are available by calling getEvaluateContext().\r\n\r\nThese changes are also applied to the ModelInfo interface.\r\n\r\nIn line with the above, ModulesFile.getDefaultInitialState() takes no arguments.\r\n\r\nIn a related change, the setUndefinedConstants() methods, which threw an\r\nexception if any constants were not defined, are deprecated. They were not in the\r\nModelInfo interface, and are not really used, e.g., because some verification\r\nmethods such as parametric might leave constants undefined, and properties file\r\nconstants are usually dealt with on a per-property basis. It is preferred to call\r\nsetSomeUndefinedConstants() instead, and problems with missing constants will be\r\npicked up at a later point.\r\n\r\n* Simplify and update \"update\" methods in simulator.\r\n\r\nReduce number of methods, removing old unused ones.\r\nMake more use of EvaluateContext for generality.\r\nAlso pass in VarList for future use (e.g., bounds checking).\r\n\r\n* Simulator fix: make resilient to reward generators not supporting transition rewards.\r\n\r\nFor example:\r\n\r\nprism -importmodel ../prism-tests/functionality/import/dice.all -ex -simpath 10 stdout\r\n\r\n* Refactoring in prism.Prism regarding model loading/storage.\r\n\r\nThis will facilitate handling models beyond symbolic/explicit\r\n(e.g., exact, parametric), which currently have limited support.\r\n\r\nIn more detail:\r\n\r\n* The current type of built model (symbolic/explicit) is stored\r\n* Querying (not setting) of the current engine is mostly now done\r\n  with new, enum-based getCurrentEngine()\r\n* Most engine-dependent choices now use either getCurrentEngine()\r\n  or check the current type of built model, not getExplicit()\r\n* The current model is cleared cleanly when passing null to model load methods\r\n* When loading a PRISM model, we don't create the ModelGenerator\r\n  until is actually needed (may need to know if it is \"exact\")\r\n* Some tidying up of the printing of model info\r\n* Rearrange code in doBuildModel: group by engine\r\n\r\n* Bug fix in TypeClock.canAssign().\r\n\r\nDoesn't show up currently since type checking for clock assignments is done separately.\r\n\r\n* Remove Prism dependency from DigitalClocks.\r\n\r\n* Alternative ASTElement.findAllConstants() taking name/type lists.\r\n\r\nAnd methods to obtain all names/objects from a Values.\r\n\r\n* Tidy up GUIInitialStatePicker in GUI simulator.\r\n\r\n- remove dependency on ModulesFile (use ModelGenerator)\r\n- process value strings with main parser, not hard-coded checks\r\n- remove duplicate state match check from GUISimulator\r\n- return state as State not Values\r\n\r\n* DigitalClocks: minor code tidying.\r\n\r\n* Remove old unused code: Modules2PTA (see 6d363beb).\r\n\r\n* Expression simplification: positions are retained for better error reporting.\r\n\r\n* PrismExceptions retain type/fields when prepending to the message.\r\n\r\nFor better error reporting.\r\n\r\n* Improved catching of model errors in GUI simulation.\r\n\r\n* ProbModel: provide static variant of convertBddToState()\r\n\r\n* Modules2MTBDD refactoring.\r\n\r\n* Use UpdateDDs data structure for translating updates\r\n* Refactor some error handling to avoid DD leaks\r\n\r\n* Add clearPosition methods to ASTElement.\r\n\r\n* GUI simulator: Refactoring and tidying for better error reporting.\r\n\r\n* Code tidying: Strategies + generics.\r\n\r\n* Code tidy + fix: Strategies + generics.\r\n\r\n* Bugfix: NPE when export of rewards to stdout is not supported.\r\n\r\n* Undeprecate setSomeUndefinedConstants(Values) in ModelInfo etc.\r\n\r\nIt is still quite a useful method to have available when you don't\r\ncare about different evaluation modes. It is used in API examples.\r\n\r\nThis is in ModelInfo (and therefore ModulesFile) and PropertiesFile.\r\nDeprecation is replaced with a more clearly explained warning instead.\r\n\r\n* Add product constructions for POMDPs. Unused for now.\r\n\r\n* Reactoring of explicit engine product constructions.\r\n\r\nThis includes construction for both DA-model products (e.g., for LTL)\r\nand product models induced by finite-memory strategies.\r\n\r\nIn both cases, we refactor the product construction code,\r\nbreaking it into two steps: model creation and model population.\r\nThis will facilitate products for later models (e.g. IMDPs).\r\n\r\n* Code tidying: generic model classes.\r\n\r\n* Relax some generic types for product models in rewards/strategies.\r\n\r\nChanges e.g. Product<? extends Model<Value>> product) to Product<?>.\r\n\r\nIt is not needed in these places, but also will cause problems later (for interval models).\r\n\r\nIn these places, the\r\n\r\n* Support for building interval models (IDTMCs and IMDPs).\r\n\r\nIn PRISM language models, transition probabilities in guards\r\ncan be defined as intervals, using the notation \"[l,u]\", where\r\nl and u are expressions that can be evaluated as doubles.\r\nThere are no explicit idtmc or imdp model keywords; instead the\r\nmodel type is inferred automatically for DTMCs or MDPs that\r\ncontain probabilities specified as intervals.\r\n\r\nIn the parser, ExpressionInterval is added to the AST classes.\r\n\r\nThe ModelGenerator interface has several new methods:\r\n * getIntervalEvaluator()\r\n * getTransitionProbabilityInterval()\r\n * getTransitionProbabilityObject()\r\n * getTransitionProbabilityString()\r\nFor the first, a new Evaluator for double intervals is added.\r\n\r\nModulesFileModelGenerator adds support for IDTMCs and IMDPs\r\nspecified in the PRISM language. This is done by making\r\nthe TransitionList and Update be of type either Value or\r\nInterval<Value>, depending on the model type, but little else\r\nis needed: generics and the new Evaluator take care of it.\r\n\r\nFor the explicit engine, we add new interfaces IDTMC and IMDP,\r\nand implementations IDTMCSimple and IMDPSimple, which are\r\nMainly just wrappers around existing classes via generic types,\r\ne.g., IDTMC<Value> extends DTMC<Interval<Value>>.\r\n\r\n* Addition of minmin/minmax/etc. to P=? and R=? in property parser.\r\n\r\n* Model checking for IDTMCs/IMDPs.\r\n\r\nFor both, we support:\r\n\r\n* probabilistic next: P[X]\r\n* probabilistic bounded reach/until: P[F<=k], P[U<=k]\r\n* probabilistic reach/until: P[F], P[U]\r\n* expected reward to reach a target: R[F]\r\n\r\nFor IDTMCs, use e.g. Pmin=? or Pmax=? to get best/worst-case values.\r\n\r\nFor IMDPs, use e.g. Pminmax=?, where the first (outer) min/max refers\r\nto the strategies/policies of the IMDP and the second (inner) to the\r\nuncertainty (selection of interval probabilities) by the environment, e.g.:\r\n\r\n* Pminmax=? = worst-case (pessimistic) minimum probability\r\n* Pminmin=? = best-case (optistic) minimum probability\r\n* Pmaxmin=? = worst-case (pessimistic) minimum probability\r\n* Pmaxmax=? = best-case (optistic) minimum probability\r\n\r\nFor IMDPs, strategy synthesis is supported in the usual way.\r\n\r\nAt the code level, MinMax is extended to specify whether min/max\r\nis required for uncertainty. Matrix multiplication methods are\r\nlabelled wirh Unc, e.g., mvMultUnc or mvMultRewUnc. This keeps\r\nthe method name spaces separate since IDTMCs/IMDPs simultaneously\r\nimplement the DTMC/MDP interfaces.\r\n\r\nVarious regression tests are added.\r\n\r\n* Explicit file model import for IDTMCs/IMDPs (explicit engine).\r\n\r\n* Allow simulation of uncertain (interval) models.\r\n\r\n* Product construction for interval models.\r\n\r\nWe implement construction for both DA-model products (e.g., for LTL)\r\nand product models induced by finite-memory strategies.\r\n\r\n* Cosafe LTL model checking (probability, rewards) for IDTMC/IMDPs.\r\n\r\n* Reducible: Implement concat as a static function.\r\n\r\nTo make code more readable, we add static functions for concatenation to Reducible:\r\n\r\nnew ChainedIterable.Of<>(iterables)\r\n\r\nbecomes: Reducible.concat(iterables)\r\n\r\nor even: concat(iterables) if concat is statically imported.\r\n\r\nCloses #222\r\n\r\n* Improve class Distribution.\r\n\r\n* Change constructors such that the Evaluator is explicit\r\n  (also deprecate Evaluator-less constructor,\r\n  add static ofDouble() creation methods\r\n  and remove setEvaluator to disallow changing of evaluator)\r\n\r\n* Implement FunctionalIterable instead of Iterable\r\n  and simplify implementation of some methods, e.g., equals, map, sum.\r\n\r\n* Fix return value of Distribution#add\r\n\r\n* Make members final\r\n\r\n* Remove old unused code that was commented out\r\n\r\n* Improve class Evaluator.\r\n\r\n* Rename methods createForXXX to forXXX for improved readability\r\n\r\n* Use singleton pattern for Double, BigRational, and DoubleInterval\r\n\r\n* Let checkProbabilityValue return the value if no Exception is thrown\r\n\r\n* Use constants for zero and one values\r\n\r\n* Minor cleanups in TypeInterval.\r\n\r\n* CHANGELOG.\r\n\r\n* Update contributor info.\r\n\r\n* Update -help message for export options.\r\n\r\n* Set default model export precision to 16 decimal places (not 17).\r\n\r\nAvoids problematic formatting due to round-off in many cases.\r\n\r\n* Fixes in Evaluator usage in Reward classes.\r\n\r\nIn particular: make sure they are copied when one Rewards object\r\nis created based on an existing one.\r\n\r\nWouldn't break at present anyway since all Rewards instances\r\nuse doubles, even for interval models.\r\n\r\n* Enable state reward export for POMDPs.\r\n\r\n* Set default strategy export type for -exportstrat based on file extension.\r\n\r\n* Strategies can provide a string view of their memory, shown in the GUI.\r\n\r\n* Make StrategyExplicit subclasses more robust when states are missing.\r\n\r\n* Improvements in finite-memory strategies from LTL products.\r\n\r\n- more robust when memory is (or becomes) unknown\r\n- refactoring and commenting in code\r\n\r\n* Improve strategy representation for POMDPs.\r\n\r\nImplements Strategy interface so works with -exportstrat\r\nand can also be simulated/exported from the GUI.\r\n\r\n* Refactor and extend strategy export options.\r\n\r\nCreate StrategyExportOptions class to manage options.\r\n\r\nThis is now passed to the various Strategy.exportX() methods\r\n(which is a change in the interface, effecting both external\r\ncalls and any other implementing classes). The exportStrategy\r\nmethods in Prism change similarly.\r\n\r\nUsing this, the -exportstrat switch, managed by PrismCL,\r\nis extended with several new options: mode, states, obs.\r\nWe also add an alias type=model for type=induced.\r\n\r\nThese options are not yet all fully supported but obs\r\ndoes now provides the choice to merge POMDP states or not.\r\n\r\n* Support states=false in -exportstates (Dot files, explicit engine).\r\n\r\n* Support reach/mode options for -exportstrat where possible (explicit).\r\n\r\n* POMDP strategy generation supports mode options (reduce,restrict) too.\r\n\r\n* Explicit model checkers copy result on inheritSettings().\r\n\r\nThis allows strategies to be stored if needed.\r\n\r\n* Only store strategy in symbolic engines is result is non-null.\r\n\r\n* Strategy generation for probabilistic next (MDPs, explicit).\r\n\r\n* Small improvements to engine auto-switching.\r\n\r\n* Don't report switch to explicit if wasn't needed\r\n* Don't switch back to MTBDD engine if had already switched to explicit\r\n\r\n* Switch to explicit engine (for now) if strategy generation requested.\r\n\r\n* Extend GUI strategies menus with \"view\" and \"simulate\".\r\n\r\n* Explicit engine model checkers no longer support -exportadv (just -exportstrat).\r\n\r\n* PrismCL: Warn about use of -exportadv for POMDPs/IMDPs/etc.\r\n\r\n* Strategy export as actions repects \"states=true\" (and this is the default).\r\n\r\n(easy to implement given that -exportstrat is is explicit-only for now)\r\n\r\n* Exand view/export strategy options in GUI.\r\n\r\n* Bugfix in POMDP product construction (unused currently).\r\n\r\n* Correcting inconsistency between state and transition reward export headers in tests.\r\n\r\n* Remove colon in transition reward export header.\r\n\r\n* Allow min/max expressions with 1 argument\r\n\r\n* Test min/max expressions with 1 argument\r\n\r\n* Strategy export: reach=false supported for FM strats, and now default for induced models.\r\n\r\n* Add -help text for -exportstrat.\r\n\r\n* Add export of (state) observations for POMDPs (and \"view\" from GUI).\r\n\r\nFrom command-line: -exportobs, or .obs extension within -exportmodel.\r\n\r\n* CHANGELOG.\r\n\r\n* Test for issue 232\r\n\r\n* Define boolean constants with one step\r\n\r\nThis fixes Issue 232.\r\nPreviously, defined boolean constants were initialized with two steps.\r\nThis causes an increment (without effec) during model checking\r\nwhich results in all properties being checked twice.\r\n\r\n* Update regression tests for recent -exportstrat finalisations.\r\n\r\n* Update Ubuntu install script (Python).\r\n\r\n* CHANGELOG.\r\n\r\n* Version number (4.8).\r\n\r\n* Update manual.\r\n\r\n* Version number (4.8.dev).\r\n\r\n* Re-enable strategy generation for IMDP bounded reachability (oops).\r\n\r\n* Align STPG class with PRISM-games.\r\n\r\n* Remove \"nested\" transition methods from STPG (only appear in STPGAbstrSimple).\r\n\r\n* Minor code tidying (compile warnings) in SPTG classes.\r\n\r\n* Fix a few JavaDoc bugs.\r\n\r\n* Remove \"nested\" transition methods from STPGRewards (not in STPG, also unused).\r\n\r\n* Fix a few JavaDoc bugs.\r\n\r\n* Bugfix in IMDP expected reward computation (wrong precomputation).\r\n\r\nPlus regression test.\r\n\r\n* IMDP export tests.\r\n\r\n* IMDP export tests.\r\n\r\n* Parametric model checker: Remove ModelBuilder reference; no longer needed.\r\n\r\n* Strategy induced model construction preserves initial states.\r\n\r\n* Documentation for StrategyExportOptions.\r\n\r\n* Switch to explicit engine for interval models (and others) works for import too.\r\n\r\nCode to switch engine moved to just before model construction,\r\nso it is also run when using, e,.g. -importmodel.\r\n\r\n* Further fix to engine switch for model import.\r\n\r\nAlso now works when the model import is not triggered by model checking.\r\n\r\n* Code tidy (compiler warnings).\r\n\r\n* Strategy: More export methods without options.\r\n\r\n* Small changes to strategy (action) export format.\r\n\r\n1. Use = not : in list. This matches other array exports, and\r\navoids potential confusion if : is used in randomised strats.\r\n\r\n2. Display \"\" not null for unlabelled actions.\r\n\r\nAlso add Strategy toString() methods, for debugging.\r\n\r\n* Retain generated strategy when solving digital clocks MDPs.\r\n\r\n* -exportpropaut also works for NBAs from non-prob LTL model checking.\r\n\r\n* Bugfix: nested R[F] properties misdetected as cosafe.\r\n\r\nE.g. for R=?[ F R>0[F s=7] ], the outer R was being misdetected\r\nas containing cosafe LTL rather than just reachability (F).\r\n\r\n* Fix detection of (syntactic) cosafe LTL (ignore nested P/R).\r\n\r\n* Change to \"make release\": don't automatically do \"make clean_all\" and \"make all\" first.\r\n\r\nThis means \"make release\" can be run directly after e.g. prism-install-ubuntu,\r\nwhich runs make at the end.\r\n\r\n* Update \"make release\" to include architecture in file name.\r\n\r\n* Update binary release filenames for Mac (e.g. osx64 -> mac64).\r\n\r\n* Implement transition reward export (MDP-like models) for explicit engine.\r\n\r\n* Fix some compiler warnings (@Deprecated).\r\n\r\n* Re-arrange simple individual test(s).\r\n\r\nUsed to check key libraries/components are installed.\r\nNow put in etc/tests so available from binary releases too.\r\nCan be run as etc/tests/run.sh.\r\nMakefile target \"make test\" now uses this too.\r\n\r\n* Fix launch scripts (was breaking on Cygwin).\r\n\r\nReinstall some quoting of variables (lost in 5251add35c).\r\nBreaks on Cygwin since PATH usually contains a space.\r\n\r\n* Update/rename install script for Fedora-based Linux (tested on Amazon Linux).\r\n\r\n* Fix for -javaparams switch.\r\n\r\n* Install script typos.\r\n\r\n* Scripts to install PRISM on a clean Windows instance.\r\n\r\nIn a Windows Command Prompt run:\r\n\r\n\"%SystemRoot%\\System32\\WindowsPowerShell\\v1.0\\powershell.exe\" -Command \"wget -Uri https://raw.githubusercontent.com/prismmodelchecker/prism/master/prism/etc/scripts/prism-install-windows.bat -Outfile prism-install-windows.bat\"\r\ncmd /K prism-install-windows.bat\r\n\r\nThen in a Cygwin terminal:\r\n\r\nwget https://raw.githubusercontent.com/prismmodelchecker/prism/master/prism/etc/scripts/prism-install-cygwin\r\nbash prism-install-cygwin\r\n\r\n* Install script typo.\r\n\r\n* Update lib README.\r\n\r\n* Add README for ext.\r\n\r\n* Easier testing that lpsolve works (make testlpsolve).\r\n\r\nOr:\r\nbin/prism etc/tests/test_lpsolve_mdpmo.prism etc/tests/test_lpsolve_mdpmo.prism.props -lp -test\r\n\r\nOr to run all:\r\netc/scripts/prism-auto -tm -p bin/prism etc/tests/\r\n\r\n* Makefile update: JAVA_DIR detection removes bin / Commands, regardless of OS.\r\n\r\nBecause, it is in bin, not Commands, now for various Mac Java installs.\r\n\r\nNote the use of sed with multiple \"-e\"s not \"|\" to work on macOS.\r\n\r\n* Makefile update: \"checks\" displays javac version.\r\n\r\n* Merge prism.darwin{32,64} launch scripts, which are identical these days.\r\n\r\n* Update prism launch script on macOS.\r\n\r\nOnly use /usr/libexec/java_home if java is in /usr/bin.\r\nThat is the problematic case for passing DYLD_LIBRARY_PATH\r\nand some Java installs do not work with /usr/libexec/java_home.\r\n\r\n* Add -javaversion switch to prism: calls \"java -version\" and exits.\r\n\r\n* prism-auto fix: Allow Nailgun usage on newer Java installs.\r\n\r\n* CI update: run build/test on macOS too, and newer Java.\r\n\r\n* Makefile fix: unit tests not working on Cygwin.\r\n\r\n* CI update: run build/test on Windows too.\r\n\r\n* Makefile fix: dos2unix bash scripts in case unpacked by Windows git.\r\n\r\n* Revert recent change to \"make release\" (now does clean first again).\r\n\r\nOtherwise, Java code does not automatically get built with --release 9.\r\n\r\n* Makefile fix: \"make release\" extends not overrides JFLAGS.\r\n\r\n* Add --nobuild option to prism-install-* scripts.\r\n\r\n* Update prism-install-ubuntu script, to avoid install interruptions.\r\n\r\n* Update prism-install-windows.bat: Run a Cygwin terminal too.\r\n\r\n* CHANGELOG update.\r\n\r\n* Switch --print-failures in prism-auto, enabled by default for \"make tests\".\r\n\r\nSometimes, CI testing generates failures that are not reproducible locally.\r\n\r\n* Patch PRISM to compile against API changes in CUDD 3.0.0.\r\n\r\n* Only need to link to libcudd, not libutil etc.\r\n* Use Cudd_NodeReadIndex to access DdNode->index\r\n* Need cuddInt.h to access internals, e.g., node ref count\r\n\r\n* Build/clean (modified) CUDD 3.0.0 from main Makefile.\r\n\r\nThis is done by calling custom scripts: install.sh and clean.sh in ../cudd.\r\nThe former takes some flags and passes them onto the configure script.\r\nWe also remove some flags/defines that were only ever needed for passing to CUDD.\r\n\r\n* Update cudd directory to 3.0.0 version (from cudd repo @ 706dea0).\r\n\r\n(i.e., from https://github.com/prismmodelchecker/cudd)\r\n\r\n* Update cudd (from repo).\r\n\r\n* Update flags passed to Makefile.\r\n\r\n* Update cudd (from repo).\r\n\r\n* Update install script - works on non-bash shells.\r\n\r\n* Remove -malign-double flag from compilation (was only there for CUDD).\r\n\r\n* Build tidy: CFLAGS/LDFLAGS.\r\n\r\nNo need for LDFLAGS to include CFLAGS.\r\nBut -static-libgcc -static-libstdc++ should be in LDFLAGS (not CFLAGS).\r\n\r\n* Build tidy: -fno-common should not be needed.\r\n\r\n* Build tidy: no particular need for -Wformat.\r\n\r\n* Build tidy: document some compiler/linker options.\r\n\r\n* Small README updates.\r\n\r\n* Small README updates.\r\n\r\n* Remove outdated Travis config.\r\n\r\n* Update make-tests.yml: newer package versions to remove warnings.\r\n\r\nNB: No longer test against Java 9 (our current minimum).\r\nJava 11 is the minimum (LTS) version available that we support.\r\n\r\n* Fix broken (command-line) transient probability computation.\r\n\r\nAnd add a regression test that would have caught it.\r\n\r\nFixes #237\r\n\r\n* Update CHANGELOG.\r\n\r\n* Update version (4.8.1).\r\n\r\n* Update manual.\r\n\r\n* Update manual.\r\n\r\n* ModelSimple construction refactoring.\r\n\r\n* Explicit engine product model construction(s) refactoring.\r\n\r\nFactor out new state creation/indexing.\r\n\r\n* Allow the simulator's random number generator to be initialised with a specific seed.\r\n\r\n* Prism API tidy: remove svn build info.\r\n\r\n* Prism API tidy: compile fix.\r\n\r\n* Version number (4.8.1.dev).\r\n\r\n* Bugfixes in MDPSimple constructor (currently unused).\r\n\r\n* Fix Linux/Mac xprism script: works when install directory has a space.\r\n\r\n* GUI simulator fix: column headings when there are variableless modules.\r\n\r\nDecision to reresh table structure was a bit too optimistic.\r\nJust disabled - performance should not be an issue here really.\r\n\r\n* Rename Type.canAssign() to canCastTypeTo().\r\n\r\n* Add Type.defaultDeclarationType() method.\r\n\r\nThis is used to allow ModelInfo.getVarDeclarationType() to be\r\nimplemented automatically in some common cases. The logic from\r\nthere is pushed into individual Type classes.\r\n\r\nWe also add DeclarationDoubleUnbounded, which is a default\r\nfor the double type. Currently no double variables are allowed\r\nbut this will later be useful for storing constant types.\r\n\r\n* Utility functions guessTypeForValue() and guessTypesForValues().\r\n\r\nThis migrates code from Values.getType() and (new) Values.getTypes()\r\nto a more sensible location in the parser.types package.\r\n\r\nThis allows refactoring of some result testing code, avoiding the need\r\nto create a ConstantList object just to infer types from Values.\r\n\r\n* Code tidy: Javadoc compiler warnings.\r\n\r\n* Tidy up some calls to VarList methods (to facilitate upcoming changes).\r\n\r\n* new method addVarAtStart(...) is preferred to addVar(0, ...)\r\n* exists(..) is preferred to getIndex(...) != -1\r\n\r\n* Update handling of constants in VarList.\r\n\r\nAn EvaluateContext is stored locally (typically obtained from\r\nModelInfo on creation of the VarList), and can be set at any\r\ntime with setEvaluateContext(). This avoids passing constant\r\nvalues to every addVar() call. It also means that the evaluation\r\nmode can also be specified if needed.\r\n\r\n* Update some VarList methods to respect current evaluation mode.\r\n\r\nNotably these methods are used to handle models with initial states.\r\n\r\n* Grammar bug fix: implication is right-associative.\r\n\r\n* Fix Expression toString() to add ()s where needed for precedence.\r\n\r\nNot a problem for parsed expressions, but it was problematic for\r\nprogramatically created ones.\r\n\r\n* Miscellaneous regression tests.\r\n\r\n* Regression testing: RESULT: Error:string checks are now case insensitive.\r\n\r\nPreviously: RESULT: Error:String would fail because the error message\r\nwas converted to lower case before testing, but not the test word(s).\r\n\r\n* Fix some broken regression tests (\"RESULT: Error\" in wrong format).\r\n\r\n* Regression test fix (export .all creates transition reward files now).\r\n\r\n* Bug fix: should throw error cleanly on exact evaluation of fractional power.\r\n\r\nAlso improve error reporting here slightly.\r\n\r\n* Add power operator a^b, equivalent to pow(a,b).\r\n\r\nFor parsing, operator precedence is immediatey below * and /,\r\nand ^ is right associative (a^b^c = a^(b^c)).\r\n\r\nThis is implemented as another case of ExpressionBinaryOp.\r\n\r\n* Add copy constructors with probability maps to core *Simple model classes.\r\n\r\n* Add/clarify hasStateRewards()/hasTransitionRewards() for Rewards().\r\n\r\n* Add copy constructors (also with maps) to core *Simple Reward classes.\r\n\r\n* DTMCEmbeddedSimple fix: copy basic model info properly.\r\n\r\n* Small change in StateRewardsSimple (avoid exceptions).\r\n\r\n* Access to DTMC/MDP transitions with probability maps.\r\n\r\nVia getTransitionsMappedIterator() methods.\r\n\r\n* Regression test bugfix: Ignore \"not supported\" before checking error match.\r\n\r\n* Small IMDP/IDTMC solution optimisation (and bugfix).\r\n\r\nSkip needless computation for trivial intervals ([1,1]).\r\n\r\nAlso fixes a bug for minimising expected reward to reach a target\r\nin IMDPs, where the max is infinite, but the min is finite.\r\nInfinite-valued choices should have value +Inf during value iteration,\r\nbut multiplying +Inf by totP=0.0 gives NaN instead.\r\nA regression test is added to check this.\r\n\r\n* Bug fix in bisimulation minimisation (quotient construction).\r\n\r\n* Distribution.equals fix (use evaluator to compare values).\r\n\r\nIn particular, this means allowing some tolerance for distributions\r\nwhere probabilities are doubles (1e-12 relative, by default).\r\n\r\nThis also allows bisimulation minimisation to factor in double\r\nimprecision too.\r\n\r\n* Code to export bisimulation minimised model (commented out).\r\n\r\n* Code tidy (Javadoc).\r\n\r\n* Bug fix in DA modifications.\r\n\r\nNow passes all PRISM regressions tests.\r\n\r\n* Fix strategy generation in MDPModelChecker.checkPartialSat.\r\n\r\n* updates to handle new prism export stragegy functionality\r\n\r\n* edits to get right engines for exporting different specs\r\n\r\n* dont tell prism to export strat using new stuff in case of multi or Rmax - still not supported on the prism side\r\n\r\n---------\r\n\r\nCo-authored-by: Dave Parker <dave.x.parker@gmail.com>\r\nCo-authored-by: Steffen Märcker <steffen.maercker@tu-dresden.de>\r\nCo-authored-by: LudwigPauly <ludwigpauly@gmail.com>\r\nCo-authored-by: Max Kurze <Max.Kurze@mailbox.tu-dresden.de>\r\nCo-authored-by: Joachim Klein <klein@tcs.inf.tu-dresden.de>","shortMessageHtmlLink":"Robots2 (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2378448564\" data-permission-text=\"Title is private\" data-url=\"https://github.com/ori-goals/prism/issues/4\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/ori-goals/prism/pull/4/hovercard\" href=\"https://github.com/ori-goals/prism/pull/4\">#4</a>)"}},{"before":"01527b0201530255ee4f208aa6299e9a6f72af2b","after":"429c63006dd7be8138a27a17c64ff84884f0b9f5","ref":"refs/heads/robots2","pushedAt":"2024-06-27T15:00:28.000Z","pushType":"push","commitsCount":3,"pusher":{"login":"bfalacerda","name":"Bruno Lacerda","path":"/bfalacerda","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4320588?s=80&v=4"},"commit":{"message":"dont tell prism to export strat using new stuff in case of multi or Rmax - still not supported on the prism side","shortMessageHtmlLink":"dont tell prism to export strat using new stuff in case of multi or R…"}},{"before":"7bb64bdd91ce1d46c3d07a7d36bb371ee106008e","after":"01527b0201530255ee4f208aa6299e9a6f72af2b","ref":"refs/heads/robots2","pushedAt":"2024-06-25T13:34:23.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"davexparker","name":"Dave Parker","path":"/davexparker","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/6075003?s=80&v=4"},"commit":{"message":"Fix strategy generation in MDPModelChecker.checkPartialSat.","shortMessageHtmlLink":"Fix strategy generation in MDPModelChecker.checkPartialSat."}},{"before":"fa0ae40decc8868ebdd24c4ce3d4f1ce23c3ba9e","after":"7bb64bdd91ce1d46c3d07a7d36bb371ee106008e","ref":"refs/heads/robots2","pushedAt":"2024-06-12T12:51:04.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"davexparker","name":"Dave Parker","path":"/davexparker","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/6075003?s=80&v=4"},"commit":{"message":"Bug fix in DA modifications.\n\nNow passes all PRISM regressions tests.","shortMessageHtmlLink":"Bug fix in DA modifications."}},{"before":null,"after":"fa0ae40decc8868ebdd24c4ce3d4f1ce23c3ba9e","ref":"refs/heads/robots2","pushedAt":"2024-06-12T11:32:03.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"davexparker","name":"Dave Parker","path":"/davexparker","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/6075003?s=80&v=4"},"commit":{"message":"Merge branch 'master' into robots","shortMessageHtmlLink":"Merge branch 'master' into robots"}},{"before":"f601dc2904dcf5440356883878892710f2437f3e","after":"7c920e06fe22266093007f400f40f71190ff5d6e","ref":"refs/heads/robots","pushedAt":"2023-12-07T16:34:03.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"bfalacerda","name":"Bruno Lacerda","path":"/bfalacerda","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4320588?s=80&v=4"},"commit":{"message":"add functionality for transient analysis","shortMessageHtmlLink":"add functionality for transient analysis"}},{"before":"f601dc2904dcf5440356883878892710f2437f3e","after":null,"ref":"refs/heads/robots2","pushedAt":"2023-10-16T17:52:58.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"bfalacerda","name":"Bruno Lacerda","path":"/bfalacerda","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4320588?s=80&v=4"}},{"before":null,"after":"f601dc2904dcf5440356883878892710f2437f3e","ref":"refs/heads/robots","pushedAt":"2023-10-16T17:52:58.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"bfalacerda","name":"Bruno Lacerda","path":"/bfalacerda","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4320588?s=80&v=4"},"commit":{"message":"change flag to export sta, lab, adv, etc files","shortMessageHtmlLink":"change flag to export sta, lab, adv, etc files"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"startCursor":"Y3Vyc29yOnYyOpK7MjAyNC0wOS0xOVQyMToxNjoyMS4wMDAwMDBazwAAAAS7U8MC","endCursor":"Y3Vyc29yOnYyOpK7MjAyMy0xMC0xNlQxNzo1Mjo1OC4wMDAwMDBazwAAAAOYScWE"}},"title":"Activity · ori-goals/prism"}