toolset issueshttps://dgit.cs.uni-saarland.de/modest/toolset/-/issues2017-08-03T11:30:50+02:00https://dgit.cs.uni-saarland.de/modest/toolset/-/issues/9declare a const array2017-08-03T11:30:50+02:00Gregory Stockdeclare a const arrayModest currently does not allow an array with a `const` / readonly modifier:
`> error: Constants cannot be of composite type.`
Background:
I have a model with very large `int`-arrays containing only constants needed for computation....Modest currently does not allow an array with a `const` / readonly modifier:
`> error: Constants cannot be of composite type.`
Background:
I have a model with very large `int`-arrays containing only constants needed for computation. Because I cannot declare them as `const`:
- `mcsta` writes them in every state of the scheduler gererated with the new `--scheduler` flag,
- `modes` writes them in my traces,
- `mosta` shows them in the global variables section (practically rendering the output useless because `dot` cannot handle this).https://dgit.cs.uni-saarland.de/modest/toolset/-/issues/12Committed Locations2017-11-15T20:12:17+01:00Gregory StockCommitted LocationsUppaal has a feature called "*committed locations*".
The [Uppaal Web Help](http://www.it.uu.se/research/group/darts/uppaal/help.php?file=System_Descriptions/Locations.shtml) describes it as follows:
> Like urgent locations, committed l...Uppaal has a feature called "*committed locations*".
The [Uppaal Web Help](http://www.it.uu.se/research/group/darts/uppaal/help.php?file=System_Descriptions/Locations.shtml) describes it as follows:
> Like urgent locations, committed locations freeze time. Furthermore, if any process is in a committed location, the next transition must involve an edge from one of the committed locations.
This has the potential of reducing the state space a lot.
For example if we have five locations where each has an enabled (and urgent) transition.
- if _none_ of them are committed, we have `5! = 120` distinct sequences
- if _one_ location is committed, we have `1! * 4! = 24` distinct sequences
- if _two_ locations are committed, we have `2! * 3! = 12` distinct sequenceshttps://dgit.cs.uni-saarland.de/modest/toolset/-/issues/14Infrastructure for integration tests2018-03-01T14:09:20+01:00Gereon Foxgfox@mpi-inf.mpg.deInfrastructure for integration testsIn order to avoid regressions, Modest needs a suite of integration tests.
These tests should consist in a collection of JANI samples that are fed to the Model Checker and analysed by it, the outcome of which is compared to an expected o...In order to avoid regressions, Modest needs a suite of integration tests.
These tests should consist in a collection of JANI samples that are fed to the Model Checker and analysed by it, the outcome of which is compared to an expected outcome. In addition, performance regressions are to be detected.
Not only do we want to use this test suite in our development workflow, but also do we want to ship it as part of the Modest package, such that users can run the test suite on their own machine (which is useful e.g. to assess Modest performance under different hardware configurations).https://dgit.cs.uni-saarland.de/modest/toolset/-/issues/16Make automata modifiable2018-02-28T15:28:42+01:00Michaela Klauckklauck@depend.uni-saarland.deMake automata modifiableAt the moment you can only create an automaton from which you know already everything, i.e. all locations, edges, ... It would be nice to be able to construct an automaton on the fly by adding locations and edges one after another.
Even ...At the moment you can only create an automaton from which you know already everything, i.e. all locations, edges, ... It would be nice to be able to construct an automaton on the fly by adding locations and edges one after another.
Even better: Be able to modify the automaton as you like, i.e. allow to delete parts of it and check its consistency directly.Sanny SchmittSanny Schmitthttps://dgit.cs.uni-saarland.de/modest/toolset/-/issues/17PRISM input and output support2019-02-26T13:16:15+01:00Arnd HartmannsPRISM input and output supportImplement support for the PRISM language (http://www.prismmodelchecker.org/manual/ThePRISMLanguage/Introduction) as an input and output formalism (i.e. lexer and parser for PRISM code, conversion from PRISM models to automata models, con...Implement support for the PRISM language (http://www.prismmodelchecker.org/manual/ThePRISMLanguage/Introduction) as an input and output formalism (i.e. lexer and parser for PRISM code, conversion from PRISM models to automata models, conversion from automata models to PRISM models, and formatting of PRISM models back to PRISM code).Sanny SchmittSanny Schmitthttps://dgit.cs.uni-saarland.de/modest/toolset/-/issues/18Smart sampling2017-11-15T14:52:39+01:00Arnd HartmannsSmart samplingImplement support for the "smart sampling" approach of Sedwards et al. (https://doi.org/10.1007/s10009-015-0383-0) in lightweight scheduler sampling for simulation of nondeterministic models. This should be both for reachability probabil...Implement support for the "smart sampling" approach of Sedwards et al. (https://doi.org/10.1007/s10009-015-0383-0) in lightweight scheduler sampling for simulation of nondeterministic models. This should be both for reachability probabilities as described in the original paper, plus a variant for expected-reward properties.https://dgit.cs.uni-saarland.de/modest/toolset/-/issues/19Simulation of steady-state properties2017-11-15T14:49:39+01:00Arnd HartmannsSimulation of steady-state propertiesThe simulator (modes tool, Simulation project) currently only handles transient properties: reachability probabilities and expected rewards. We need to add support for steady-state properties (the S operator in CSL), both for classic Mon...The simulator (modes tool, Simulation project) currently only handles transient properties: reachability probabilities and expected rewards. We need to add support for steady-state properties (the S operator in CSL), both for classic Monte Carlo simulation as well as for rare event simulation.https://dgit.cs.uni-saarland.de/modest/toolset/-/issues/21Modest language guide2017-11-15T14:59:19+01:00Arnd HartmannsModest language guideCreate a Modest language guide for the modestchecker.net website, similar to the documentation of the PRISM language at http://www.prismmodelchecker.org/manual/ThePRISMLanguage/Introduction.Create a Modest language guide for the modestchecker.net website, similar to the documentation of the PRISM language at http://www.prismmodelchecker.org/manual/ThePRISMLanguage/Introduction.https://dgit.cs.uni-saarland.de/modest/toolset/-/issues/22Use properties instead of fields for the state struct in compiled exploration2018-03-02T15:58:55+01:00Arnd HartmannsUse properties instead of fields for the state struct in compiled explorationCurrently, the locations and state variables of a model are compiled as fields into the state struct type in compiled exploration (in the Exploration project). This is inflexible since the way that values are stored cannot be changed ind...Currently, the locations and state variables of a model are compiled as fields into the state struct type in compiled exploration (in the Exploration project). This is inflexible since the way that values are stored cannot be changed independently of how the values are accessed. We should instead implement properties for the fields and only access (get and set) them via these properties. As a second step, this will allow more advanced storage, e.g. bit-packing multiple state variables into a single (short, int, long etc.) field of the struct.https://dgit.cs.uni-saarland.de/modest/toolset/-/issues/24Assignments native2018-06-21T17:40:28+02:00Holger HermannsAssignments nativeAt the end of Sec 6 of the [2006 Modest paper](http://www-i2.informatik.rwth-aachen.de/pub/index.php?type=download&pub_id=220) some abbreviations are defined.
It seems (at least) this one is not supported in the current version.
> I...At the end of Sec 6 of the [2006 Modest paper](http://www-i2.informatik.rwth-aachen.de/pub/index.php?type=download&pub_id=220) some abbreviations are defined.
It seems (at least) this one is not supported in the current version.
> In a similar line, conventional like `y := 3;` are to be read as `{= y:=3 =};`
It would be good to have that built in. The intention is that standard sequential programming (including also while/for etc) have native support in Modest (albeit at the price of inducing many internal transitions, which can be optimised away by good static analysis/compilation).Gereon Foxgfox@mpi-inf.mpg.deGereon Foxgfox@mpi-inf.mpg.dehttps://dgit.cs.uni-saarland.de/modest/toolset/-/issues/25scheduling transitions, not actions2018-01-03T11:47:08+01:00Holger Hermannsscheduling transitions, not actionsIn order to avoid that a scheduler (as exported currently from mcsta) may induce nondeterminism (since it currently maps to actions), it appears more handy to instead map to pairs of action and target distribution, so as to enable the re...In order to avoid that a scheduler (as exported currently from mcsta) may induce nondeterminism (since it currently maps to actions), it appears more handy to instead map to pairs of action and target distribution, so as to enable the reconstruction of the exact transition taken.https://dgit.cs.uni-saarland.de/modest/toolset/-/issues/28Disabling console output, especially the progress bar2017-12-08T23:29:54+01:00Michaela Klauckklauck@depend.uni-saarland.deDisabling console output, especially the progress barAs far as the Modest people in Saarbrücken know, there is no way to disable the console output, especially the progress bar. For some purposes, like e.g. for debugging, but also for other applications where no statistics etc. are used, i...As far as the Modest people in Saarbrücken know, there is no way to disable the console output, especially the progress bar. For some purposes, like e.g. for debugging, but also for other applications where no statistics etc. are used, it would be great to have a flag or a parameter to enable/disable the output. More concrete this is sometimes necessary, because the progress bar can be interleaved by other outputs, which then are partially overwritten. In addition the progress bar causes crashes of the execution if the console window is resized/moved to another window during execution on linux.https://dgit.cs.uni-saarland.de/modest/toolset/-/issues/31String Representation of States in mcsta Scheduler2018-12-18T18:39:14+01:00Gregory StockString Representation of States in mcsta SchedulerI recently encounter a problem concerning the variable order in the states of a scheduler generated by `mcsta`.
The position of some variables in different schedulers for the "same" model (the structure is identical, only some initial va...I recently encounter a problem concerning the variable order in the states of a scheduler generated by `mcsta`.
The position of some variables in different schedulers for the "same" model (the structure is identical, only some initial variable/array values change) vary.
Context:
I use `modes` to simulate a modest model according to the `mcsta` scheduler in order to receive the optimal trace implicitely calculated by the model checker.
I currently rely on the position of the variables because otherwise I cannot distinguish between the `location` of all instances of the same process given that they all have the same name, e.g. `Experiment.location`.
In the previous model version, only the position of the global clock `gc` deterministically changed between the representation in the scheduler and the internal representation in `modes`[^1] / order in the output trace.
This allowed for a simple fix that deterministically moved the affected entries to their correct place.
This is yet not possible anymore as not even the order *within the schedulers* is predictable.
Example (first entry of the two schedulers):
```
+ State: (AttitudeControl.location = 0, Experiment.location = 0, Experiment.location = 0, Experiment.location = 0, Experiment.location = 0, Experiment.location = 0, Experiment.location = 0, Experiment.location = 0, Exp_Provider.location = 0, Exp_Provider.location = 0, Exp_Provider.location = 0, Exp_Provider.location = 0, Exp_Provider.location = 0, Exp_Provider.location = 0, Exp_Provider.location = 0, Battery.location = 0, Sun.location = 0, Main.location = 0, GlobalInvariant.location = 0, GlobalSync.location = 0, a = 1, ratio = 0, AttitudeControl.a_dst = 0, gc = 0, new_time = 0, AttitudeControl.slewingEnd_time = 0, Battery.old_time = 0, ac_lock = False, slewing = False, insolation = False, Sun.updateAfterInsolationEnd = False, cost = 0, l = 134784000, sun_c = 0, Battery.r = 0, c = [0, 0, 0, 0, 0, 0, 0], nee = [0, 0, 0, 0, 0, 0, 0], pa = [False, False, False, False, False, False, False])
|============================================================================================================================================================================================================================|
+ State: (AttitudeControl.location = 0, Experiment.location = 0, Experiment.location = 0, Experiment.location = 0, Experiment.location = 0, Experiment.location = 0, Experiment.location = 0, Experiment.location = 0, Exp_Provider.location = 0, Exp_Provider.location = 0, Exp_Provider.location = 0, Exp_Provider.location = 0, Exp_Provider.location = 0, Exp_Provider.location = 0, Exp_Provider.location = 0, Battery.location = 0, Sun.location = 0, Main.location = 0, GlobalInvariant.location = 0, GlobalSync.location = 0, a = 1, ratio = 0, AttitudeControl.a_dst = 0, ac_lock = False, slewing = False, insolation = False, Sun.updateAfterInsolationEnd = False, gc = 0, cost = 0, l = 134784000, new_time = 0, sun_c = 0, AttitudeControl.slewingEnd_time = 0, Battery.r = 0, Battery.old_time = 0, c = [0, 0, 0, 0, 0, 0, 0], nee = [0, 0, 0, 0, 0, 0, 0], pa = [False, False, False, False, False, False, False])
```
How is the variable order in the scheduler states determined? And is it possible to keep it fixed for the same model (only with different variable assignments) or even to ensure the same order within `mcsta`'s schedulers and `modes`' traces?
[^1]: for example the `toString()` of `ref T currentState` in `Simulation/Runs/STASimulationRun.cs`https://dgit.cs.uni-saarland.de/modest/toolset/-/issues/41Move code formatting rules to solution / project files2018-03-07T12:07:19+01:00Felix FreibergerMove code formatting rules to solution / project filesAs discussed in the meeting, we want to align the coding guidelines with Visual Studio defaults and settings stored within the solution or project files.
Steps needed for this:
* [x] investigate how and which settings can be configure...As discussed in the meeting, we want to align the coding guidelines with Visual Studio defaults and settings stored within the solution or project files.
Steps needed for this:
* [x] investigate how and which settings can be configured for the project (@fefrei)
* [ ] make appropriate adjustments to the coding guidelines (@gfox, @ahartmanns)
* [ ] apply the adjusted guidelines to the projectGereon Foxgfox@mpi-inf.mpg.deGereon Foxgfox@mpi-inf.mpg.dehttps://dgit.cs.uni-saarland.de/modest/toolset/-/issues/42Make interval arithmetic handle empty intervals gracefully2018-02-28T07:42:49+01:00Gereon Foxgfox@mpi-inf.mpg.deMake interval arithmetic handle empty intervals gracefullyRight now if you have two intervals `a` and `b` and one of them is empty, the operations `a + b` and `a - b` throw an `ArgumentOutOfRangeException.`. Making these operations simply return an empty interval instead would simplify calling ...Right now if you have two intervals `a` and `b` and one of them is empty, the operations `a + b` and `a - b` throw an `ArgumentOutOfRangeException.`. Making these operations simply return an empty interval instead would simplify calling code and actually fits the semantics of intervals well ("The sum of `a` and `b` is the interval of all values `x + y` for `x` from `a` and `y` from `b`").
I therefor suggest we make these operation return empty intervals in said case. I already tried to check if the exceptions are handled anywhere, which does not seem to be the case.
Any reason not to do it?Gereon Foxgfox@mpi-inf.mpg.deGereon Foxgfox@mpi-inf.mpg.dehttps://dgit.cs.uni-saarland.de/modest/toolset/-/issues/43Licensing2018-03-26T17:08:55+02:00Michaela Klauckklauck@depend.uni-saarland.deLicensingBecause more and more students and other developers contribute to the Modest Toolset, we should set up a CLA and ask previous contributors to sign it retroactively. At the moment there is no concrete license for Modest, only that it is n...Because more and more students and other developers contribute to the Modest Toolset, we should set up a CLA and ask previous contributors to sign it retroactively. At the moment there is no concrete license for Modest, only that it is not open source. This issue should be discussed as soon as possible as long as all developers can be reached.Arnd HartmannsArnd Hartmannshttps://dgit.cs.uni-saarland.de/modest/toolset/-/issues/44Support complex initial state specifications2018-03-12T10:12:27+01:00Michaela Klauckklauck@depend.uni-saarland.deSupport complex initial state specificationsWhen restricting the initial state using an arithmetic expression (over global variables `q1, q2, q3` in this case), the error message:
> error: Complex initial states specifications are not yet supported.
is thrown.
It would be nice ...When restricting the initial state using an arithmetic expression (over global variables `q1, q2, q3` in this case), the error message:
> error: Complex initial states specifications are not yet supported.
is thrown.
It would be nice to extend the range of supported expressions because in e.g. PRISM case studies they are used very often.
` "restrict-initial":{
"exp":{
"op":"≥",
"left":{
"op":"+",
"left":{
"op":"+",
"left":"q1",
"right":"q2"
},
"right":"q3"
},
"right":1
}
},`
The currently supported syntax for initial state restrictions is checked in `DissectInitialStatesRestriction()` in `AutomataNetwork.cs`. And the error message is thrown in ` CreateSetInitialStateAndTransients()` in `CompiledAutomaton.cs`https://dgit.cs.uni-saarland.de/modest/toolset/-/issues/45Support more than one initial state2018-03-12T13:38:26+01:00Michaela Klauckklauck@depend.uni-saarland.deSupport more than one initial stateModest does currently not support more than one initial state. This means that initial state restrictions using disjunctions or shrinking variables to a certain range are not allowed. Therefore this issue is in some sense related to #44....Modest does currently not support more than one initial state. This means that initial state restrictions using disjunctions or shrinking variables to a certain range are not allowed. Therefore this issue is in some sense related to #44.
A workaround would be to add a dummy initial state with tau transitions to all other real initial states. But since PRISM supports this feature, all JANI translations from such PRISM models will result in Jani files not directly (without a preprocessing step adding the dummy initial state) supported by Modest.https://dgit.cs.uni-saarland.de/modest/toolset/-/issues/46Support for safety LTL fragment2018-04-11T16:08:06+02:00Arnd HartmannsSupport for safety LTL fragmentA subset of LTL can be decided with observer automata that do not make use of omega conditions like Büchi etc. Properties using this subset could be supported in all analysis tools by adding an automata transformation that adds such an o...A subset of LTL can be decided with observer automata that do not make use of omega conditions like Büchi etc. Properties using this subset could be supported in all analysis tools by adding an automata transformation that adds such an observer and simplifies the corresponding property to a reachability property.Sanny SchmittSanny Schmitthttps://dgit.cs.uni-saarland.de/modest/toolset/-/issues/49Support for expected rate rewards in Markov automata model checking2018-06-16T00:57:54+02:00Arnd HartmannsSupport for expected rate rewards in Markov automata model checkingMarkov automata model checking in the ModelChecking project is currently only implemented for unbounded reachability and expected transition reward properties.
Task: Implement support for unbounded expected rate reward properties. I fir...Markov automata model checking in the ModelChecking project is currently only implemented for unbounded reachability and expected transition reward properties.
Task: Implement support for unbounded expected rate reward properties. I first thought this can be done symbolically (i.e. on the automata network level), but due to guards and maximal progress disabling Markovian transitions, it may rather need to be integrated into state space exploration.Arnd HartmannsArnd Hartmannshttps://dgit.cs.uni-saarland.de/modest/toolset/-/issues/50Transform STA models that are actually MA into real MA models with rates2018-06-16T00:59:19+02:00Arnd HartmannsTransform STA models that are actually MA into real MA models with ratesThis should be doable with a symbolic transformation (i.e. on the level of the automata network).This should be doable with a symbolic transformation (i.e. on the level of the automata network).Arnd HartmannsArnd Hartmannshttps://dgit.cs.uni-saarland.de/modest/toolset/-/issues/51Use NetworkCompilerHelper instead of compiling manually in motest2018-07-08T16:55:47+02:00Arnd HartmannsUse NetworkCompilerHelper instead of compiling manually in motestmotest currently manages all the steps of compiling an `AutomataNetwork` manually. This prevents better encapsulation of the compilation process in the Exploration project. It should be possible with very limited effort to make motest us...motest currently manages all the steps of compiling an `AutomataNetwork` manually. This prevents better encapsulation of the compilation process in the Exploration project. It should be possible with very limited effort to make motest use `NetworkCompilerHelper.Compile` and related methods instead.Alexander Graf-BrillAlexander Graf-Brillhttps://dgit.cs.uni-saarland.de/modest/toolset/-/issues/54Implement support for array equality comparisons2018-11-07T21:53:35+01:00Arnd HartmannsImplement support for array equality comparisonsAdd support for comparing entire arrays, e.g. `[3, 3, 3] == array(i, 3, 3)` should evaluate to `true`.Add support for comparing entire arrays, e.g. `[3, 3, 3] == array(i, 3, 3)` should evaluate to `true`.Arnd HartmannsArnd Hartmannshttps://dgit.cs.uni-saarland.de/modest/toolset/-/issues/55mosta: dot sometimes fails with full state labels2019-02-07T18:28:25+01:00Arnd Hartmannsmosta: dot sometimes fails with full state labelsWhen running
`mosta "Case Studies\pta\brp.modest" -O out.dot -D png out.png -Y --no-transient-values -E`
dot does not produce an output png file and mosta consequently crashes. With `-S`, it works.
1. Fix the crash.
2. Check if the r...When running
`mosta "Case Studies\pta\brp.modest" -O out.dot -D png out.png -Y --no-transient-values -E`
dot does not produce an output png file and mosta consequently crashes. With `-S`, it works.
1. Fix the crash.
2. Check if the reason for dot failure is in the dot file generated by mosta, and if yes, fix it.https://dgit.cs.uni-saarland.de/modest/toolset/-/issues/57Recursive process calls fails because of too strict checking2019-02-25T14:12:07+01:00Hans van der LaanRecursive process calls fails because of too strict checkingWhen running the code below, we get the following error: figure-3-15-process_decl.modest:(16,28): error: Cannot read local variables or process parameters immediately before a recursive process call.
If I interpreted Arnd's critique cor...When running the code below, we get the following error: figure-3-15-process_decl.modest:(16,28): error: Cannot read local variables or process parameters immediately before a recursive process call.
If I interpreted Arnd's critique correctly, in this case we should be able to make a recursive process call since we don’t change the variable.
```
//---Property which should always hold---
const int check = 1;
property Term = Pmin(<> (check == 1)) == 1;
//---------------------------------------
action snd_data, rcv_ack, timeout;
exception err;
int n = 3;
process Sender(int n)
{
snd_data {= n = n - 1 =};
alt {
:: rcv_ack
:: timeout; alt {
:: when(n > 0) Sender(n)
:: when(n == 0) throw(err)
}
}
}
Sender(2)
```https://dgit.cs.uni-saarland.de/modest/toolset/-/issues/63Tau (τ) shown as 't' on windows2019-03-07T10:36:17+01:00Hans van der LaanTau (τ) shown as 't' on windowsWindows displays 't' instead of 'τ' (tau) in error messages.
This can cause confusion for users when they get error messages such as `Encountered temporal nondeterminism for t.`, as they will perhaps not make the connection that 't' is...Windows displays 't' instead of 'τ' (tau) in error messages.
This can cause confusion for users when they get error messages such as `Encountered temporal nondeterminism for t.`, as they will perhaps not make the connection that 't' is actually the τ action. This was the case when I started learning Modest.https://dgit.cs.uni-saarland.de/modest/toolset/-/issues/64State space export: include rates of Markovian transitions2019-03-11T15:07:14+01:00Arnd HartmannsState space export: include rates of Markovian transitionsThe new state space export functionality of mcsta currently ignores the rates of Markovian transitions completely. It should instead output them in addition to the action label.The new state space export functionality of mcsta currently ignores the rates of Markovian transitions completely. It should instead output them in addition to the action label.Hans van der LaanHans van der Laanhttps://dgit.cs.uni-saarland.de/modest/toolset/-/issues/65Evaluate use of Roaring Bitmaps for bitsets2019-03-11T17:57:07+01:00Arnd HartmannsEvaluate use of Roaring Bitmaps for bitsetsTest whether using Roaring Bitmaps - https://roaringbitmap.org/, https://github.com/RogueException/CRoaring.Net, https://github.com/Tornhoof/RoaringBitmap - improves performance or memory usage significantly in model checking.Test whether using Roaring Bitmaps - https://roaringbitmap.org/, https://github.com/RogueException/CRoaring.Net, https://github.com/Tornhoof/RoaringBitmap - improves performance or memory usage significantly in model checking.https://dgit.cs.uni-saarland.de/modest/toolset/-/issues/68Add initial/deadlock/absorbing atomic properties to explored states2019-03-17T20:17:36+01:00Hans van der LaanAdd initial/deadlock/absorbing atomic properties to explored statesWhen we start the state space exploration, we know which state is the intial state. Furthermore, during state space exploration we can observe if a given state deadlocks or if it's absorbing.
These state-instrinsic properties could help...When we start the state space exploration, we know which state is the intial state. Furthermore, during state space exploration we can observe if a given state deadlocks or if it's absorbing.
These state-instrinsic properties could help users to verify interesting properties about their model.https://dgit.cs.uni-saarland.de/modest/toolset/-/issues/71Duplicate properties get skipped silently2019-03-21T13:49:51+01:00Hans van der LaanDuplicate properties get skipped silentlyAt the moment, duplicate properties are skipped silently. We should inform the user that a given property is being skipped.
This could be especially useful in the case the user doesn't know 2 properties are equivalent (for example, in ...At the moment, duplicate properties are skipped silently. We should inform the user that a given property is being skipped.
This could be especially useful in the case the user doesn't know 2 properties are equivalent (for example, in the case that we rewrite a property underwater). I encountered this when writing some very basic properties for bug hunting, and to my surprise not all properties showed up on the output.
**Model:**
```
property p_1 = Pmin(<> true);
property p_2 = Pmin(<> true);
property p_3 = Pmin(<> false);
process RandomWalk()
{
int i;
tau palt {
:6: {= i = (i + 1) % 5 =}; RandomWalk()
:4: {= =}; RandomWalk()
}
}
RandomWalk()
```
**Output:**
```
[...]
+ State space exploration
State size: 1 bytes
States: 1
Transitions: 1
Branches: 2
Rate: 15 states/s
Time: 0.1 s
+ Property p_1
Probability: 1
Bounds: [1, 1]
Time: 0.0 s
+ Value iteration
Final error: 0
Iterations: 1
Time: 0.0 s
+ Property p_3
Probability: 0
Bounds: [0, 0]
Time: 0.0 s
+ Value iteration
Final error: 0
Iterations: 1
Time: 0.0 s
```https://dgit.cs.uni-saarland.de/modest/toolset/-/issues/72Add reference to QComp on Modest Sample Page2019-04-04T15:07:14+02:00Hans van der LaanAdd reference to QComp on Modest Sample PageWe should add a link to the example page stating that more Modest models can be found in the QComp benchmark set.We should add a link to the example page stating that more Modest models can be found in the QComp benchmark set.https://dgit.cs.uni-saarland.de/modest/toolset/-/issues/74Add contextual information to “The rate of a Markovian transition is zero or ...2019-04-04T15:20:30+02:00Hans van der LaanAdd contextual information to “The rate of a Markovian transition is zero or negative.” error.The “The rate of a Markovian transition is zero or negative.” error currently gives the user no contextual information of where or why this is happening in their model. Having this makes it much easier for them to debug this error.
As ...The “The rate of a Markovian transition is zero or negative.” error currently gives the user no contextual information of where or why this is happening in their model. Having this makes it much easier for them to debug this error.
As an example, we can trigger this error in the bitoin-attack model from the case studies by giving it the parameters: ```-E "MALICIOUS = 20, CD = 6"```.https://dgit.cs.uni-saarland.de/modest/toolset/-/issues/75Provide a counterexample when we cannot calculate a max. expected reward beca...2019-04-28T19:29:12+02:00Hans van der LaanProvide a counterexample when we cannot calculate a max. expected reward because Pmin < 1https://dgit.cs.uni-saarland.de/modest/toolset/-/issues/76Self-loop goes to state -1 in DOT export2021-03-24T19:20:50+01:00Hans van der LaanSelf-loop goes to state -1 in DOT export**Description:**
When exporting the following model to DOT, we obtain an incorrect visualization.
We should have a self loop in state 6, not a transition to state -1.
**Model:**
```
action act;
int reward = 0;
int global_state = 0;
bo...**Description:**
When exporting the following model to DOT, we obtain an incorrect visualization.
We should have a self loop in state 6, not a transition to state -1.
**Model:**
```
action act;
int reward = 0;
int global_state = 0;
bool final = false;
property dummy = Pmin(<> (global_state == 5));
process Server(int state)
{
alt {
:: when(state == 0) act palt {
:0.5: {= state = 1, global_state = 1 =}
:0.5: {= state = 2, global_state = 2 =}
}
:: when(state == 1) act {= state = 3, global_state = 3 =}
:: when(state == 2) act {= state = 3, global_state = 3 =}
:: when(state == 3) act;
palt {
:0.4: {= state = 3, global_state = 3 =}
:0.4: {= state = 4, global_state = 4 =}
:0.2: {= state = 2, global_state = 2 =}
}
:: when(state == 4) act palt {
:0.5: {= state = 4, global_state = 4 =}
:0.5: {= state = 5, global_state = 5 =}
}
:: when(state == 5) act {= final = true =} //self loop
};
Server(state)
}
Server(0)
```
**Image:**
![image](/uploads/6363e0fa5618bce39ed9b8293188b5e4/image.png)https://dgit.cs.uni-saarland.de/modest/toolset/-/issues/77Overflow in arithmetic operation when running reward-bounded algorithm2019-05-01T08:43:50+02:00Zhen ZhangOverflow in arithmetic operation when running reward-bounded algorithmAn arithmetic overflow exception was generated when running the command below on the attached modest model. I listed my machine spec and other information that might be helpful for diagnosis. [abstractArbiter25state_234.modest](/uploads/...An arithmetic overflow exception was generated when running the command below on the attached modest model. I listed my machine spec and other information that might be helpful for diagnosis. [abstractArbiter25state_234.modest](/uploads/0e25d1b42362d00a77c3625fe5d82ccc/abstractArbiter25state_234.modest)
>> mcsta abstractArbiter25state_234.modest -S Memory --reward-bounded-alg StateElimination --alg IntervalIteration > output.txt
OS: Darwin Kernel Version 18.5.0, MacOS Mojave version 10.14.4
processor: 2.7 GHz Intel Core i7
memory: 16 GB 2133 MHz LPDDR3
Contents written to output.txt:
abstractArbiter25state_234.modest: info: abstractArbiter25state_234 is a DTMC model.
abstractArbiter25state_234.modest: info: Need 8 bytes per state.
abstractArbiter25state_234.modest: info: Explored 80158413 states.
Terminal printout:
[ERROR] FATAL UNHANDLED EXCEPTION: System.OverflowException: Arithmetic operation resulted in an overflow.
at Modest.StateSpace.Memory..ctor (System.Int64 length, System.Boolean zeroMemory) [0x0001d] in <addc782f107d479594b45cbe13e1e356>:0
at Modest.StateSpace.Partition.Merge (Modest.StateSpace.Partition[] partitions, Modest.Modularity.OperationState operationState, System.String experimentStatusString) [0x007b2] in <addc782f107d479594b45cbe13e1e356>:0
at Modest.StateSpace.PartitionedStateSpace.MergePartitions (Modest.Modularity.OperationState operationState, System.String experimentStatusString) [0x0000b] in <addc782f107d479594b45cbe13e1e356>:0
at Modest.ModelChecking.MAModelChecker`1[T].ModelCheck (System.String experimentString, Modest.Modularity.OperationState operationState, Modest.Modularity.ComponentErrorHandler ceh) [0x00905] in <704ceaa1ee80407c8d44bad47ced74d3>:0
at Modest.ModelChecking.ModelCheckingAnalysisEngine.ModelCheckGeneric[T] (Modest.Exploration.Network`1[T] network, System.Object expInfoObj, System.String experimentString, Modest.StateSpace.StateProjections projections, System.Object propertiesObj, Modest.StateSpace.ComponentisedExpression[] distanceExps, System.Object parametersObj, Modest.Modularity.ILocation documentLocation, Modest.Modularity.OperationState operationState, Modest.Modularity.ComponentErrorHandler ceh) [0x000b5] in <704ceaa1ee80407c8d44bad47ced74d3>:0
at (wrapper delegate-invoke) type_16777215.invoke_AnalysisDataSet_Network`1<State1>_object_string_StateProjections_object_ComponentisedExpression[]_object_ILocation_OperationState_ComponentErrorHandler(Modest.Exploration.Network`1<CompiledAutomata.State1>,object,string,Modest.StateSpace.StateProjections,object,Modest.StateSpace.ComponentisedExpression[],object,Modest.Modularity.ILocation,Modest.Modularity.OperationState,Modest.Modularity.ComponentErrorHandler)
at invoke Modest.Exploration.Network`1__CompiledAutomata.State1\, CompiledAutomata10890767824702885931\, Version=0.0.0.0\, Culture=neutral\, PublicKeyToken=null__ : System.Object : System.String : Modest.StateSpace.StateProjections : System.Object : Modest.StateSpace.ComponentisedExpression__ : System.Object : Modest.Modularity.ILocation : Modest.Modularity.OperationState : Modest.Modularity.ComponentErrorHandler : Modest.Modularity.AnalysisDataSet.GeneratedClass.DoInvoke (System.Object , System.Object[] , System.Reflection.MethodInfo ) [0x00011] in <9dfaedfc16e24eca93fb767fe015ac98>:0
at Modest.DirectInvoker.InvokeDirect (System.Reflection.MethodInfo method, System.Object instance, System.Object[] parameters) [0x00189] in <d552551992da4170a64bbd79ca19b534>:0
at Modest.Exploration.NetworkGenericMethod.Invoke (System.Object network) [0x00021] in <580459dfc38f412089709c03e6616f76>:0
at Modest.ModelChecking.ModelCheckingAnalysisEngine.ModelCheck (Modest.Automaton.NSHAModel model, Modest.ModelChecking.ModelCheckingAnalysisEngine+CompilationParameters compilationParams, System.Object parametersObj, Modest.Modularity.OperationState operationState, Modest.Modularity.IErrorHandler errors) [0x009d5] in <704ceaa1ee80407c8d44bad47ced74d3>:0
at Modest.ModelChecking.ModelCheckingAnalysisEngine.Analyze (Modest.ModelChecking.ModelCheckingAnalysisEngine+AnalysisParams analysisParameters, Modest.Automaton.NSHAModel model, System.Collections.Generic.IEnumerable`1[T] modelParameters, Modest.Modularity.OperationState operationState, Modest.Modularity.IErrorHandler errors) [0x00b94] in <704ceaa1ee80407c8d44bad47ced74d3>:0
at Modest.Modularity.AnalysisEngine`3[M,EP,AP].Analyze (Modest.Modularity.IParameterObject analysisParameters, Modest.Modularity.IModel model, System.Collections.Generic.IEnumerable`1[T] experiments, Modest.Modularity.OperationState operationState, Modest.Modularity.IErrorHandler errors) [0x00114] in <ef86b51dec5c44d39762fff3a72ce7be>:0
at Modest.Executables.Mcsta.Program.Run (Modest.Executables.Mcsta.Program+McstaParams parameters, System.Diagnostics.Stopwatch time) [0x00442] in <3c13b72722034516b619c5d85146d367>:0
at Modest.Executables.Mcsta.Program.Main (System.String[] args) [0x0007a] in <3c13b72722034516b619c5d85146d367>:0https://dgit.cs.uni-saarland.de/modest/toolset/-/issues/81Show converging bounds with interval iteration2019-05-21T14:20:53+02:00Hans van der LaanShow converging bounds with interval iteration![image](/uploads/1d886ce94102939098402802d9f6238a/image.png)
At the moment, we only show the width of the converging bounds. We should display the converging bounds themselves too.
With this feature, a user can get an impression wher...![image](/uploads/1d886ce94102939098402802d9f6238a/image.png)
At the moment, we only show the width of the converging bounds. We should display the converging bounds themselves too.
With this feature, a user can get an impression where the value is converging to.
Imagine a user is making a model, adds a property and observes it's converging to 400 while it should converge to 4. In this case, the user knows something is wrong before full conversion has been reached and can end the checking prematurely.https://dgit.cs.uni-saarland.de/modest/toolset/-/issues/82Case study cashier.modest cannot be parsed by mcsta2019-05-21T14:22:14+02:00Hans van der LaanCase study cashier.modest cannot be parsed by mcstaThe cashier.modest case study from the modes models cannot be parsed by mcsta.
We get the following error when we try to check the model with mcsta:
```
cashier.modest:(40,15): error: Expected "S", "T" or "X".
```The cashier.modest case study from the modes models cannot be parsed by mcsta.
We get the following error when we try to check the model with mcsta:
```
cashier.modest:(40,15): error: Expected "S", "T" or "X".
```https://dgit.cs.uni-saarland.de/modest/toolset/-/issues/85modes: RES: ad hoc specification of threshold levels and splitting2019-06-11T19:05:26+02:00Carlos Estebanmodes: RES: ad hoc specification of threshold levels and splittingIn the modes commands for rare event simulation, make --levels accept a string of pairs "t1,s1 t2,s2 ... tn,sn" (in whatever syntax is convenient).
All pairs should be numbers: "ti,si" means that the i-th threshold used for RES is set at...In the modes commands for rare event simulation, make --levels accept a string of pairs "t1,s1 t2,s2 ... tn,sn" (in whatever syntax is convenient).
All pairs should be numbers: "ti,si" means that the i-th threshold used for RES is set at importance value "ti," and that the splitting to perform there is "si."Arnd HartmannsArnd Hartmannshttps://dgit.cs.uni-saarland.de/modest/toolset/-/issues/86Intermediate Probabilities Completely Fill Console2019-07-04T15:06:48+02:00Hans van der LaanIntermediate Probabilities Completely Fill Console**Problem:**
When calculating the 'P_MWinMax` property from 'bitcoin-attack.modest', the command line interface completely fills up with all 10.000 intermediate probabilities. We probably do not want to show all intermediate probabiliti...**Problem:**
When calculating the 'P_MWinMax` property from 'bitcoin-attack.modest', the command line interface completely fills up with all 10.000 intermediate probabilities. We probably do not want to show all intermediate probabilities when the user does not specifically ask for this.
An idea could print the first and last 100 probabilities, with a message accompanying the output stating that to get all intermediate probabilities the '-D' parameter should be added.
**Property:**
P_MWinMax = Pmax(<>[S(round)<=10000] (m_len >= CD && m_diff > 0)); the following property completely fills up
**Output:**
```
[...]
(3022, 0.288204053592764), (3023, 0.288284334303679), (3024, 0.288364605960044),
(3025, 0.288444868562878), (3026, 0.288525122113205), (3027, 0.288605366612044),
(3028, 0.288685602060416), (3029, 0.288765828459343), (3030, 0.288846045809844),
(3031, 0.288926254112941), (3032, 0.289006453369653), (3033, 0.289086643581002),
[...]
(9993, 0.675750001988019), (9994, 0.675786572890798), (9995, 0.675823139668887),
(9996, 0.67585970232275), (9997, 0.675896260852853), (9998, 0.67593281525966),
(9999, 0.675969365543638), (10000, 0.67600591170525)
}
Time: 0.3 s
+ Value iteration
Final error: 0
Iterations: 29996
Time: 0.2 s
PS C:\Users\Gebruiker\Documents\Werk\Modest\GitLab\toolset\Binaries\Release>
```https://dgit.cs.uni-saarland.de/modest/toolset/-/issues/90ArgumentException on empty palt in Modest2020-10-16T16:15:06+02:00Arnd HartmannsArgumentException on empty palt in ModestThe following Modest code causes the tools to crash with an ArgumentException due to the empty `palt` construct:
```
property p = Pmin(<> (i > 10));
int i = 0;
process increment() {
{= i++ =};
palt {}
}
increment()
```
(Repor...The following Modest code causes the tools to crash with an ArgumentException due to the empty `palt` construct:
```
property p = Pmin(<> (i > 10));
int i = 0;
process increment() {
{= i++ =};
palt {}
}
increment()
```
(Reported by Gerlof Bouma.)https://dgit.cs.uni-saarland.de/modest/toolset/-/issues/91Default values for constants2020-11-25T19:27:17+01:00Arnd HartmannsDefault values for constantsCurrently, a constant in Modest and JANI either has a value assigned in the model, or it is open - then a value has to be specified on the command line for all tools in the Modest Toolset (or one could use a parametric analysis with e.g....Currently, a constant in Modest and JANI either has a value assigned in the model, or it is open - then a value has to be specified on the command line for all tools in the Modest Toolset (or one could use a parametric analysis with e.g. Storm). It would be convenient to be able to define a "default value" for (some) constants in a model, so that they take this value _unless_ one is specified on the command line. This would be an extension to both Modest and JANI.https://dgit.cs.uni-saarland.de/modest/toolset/-/issues/93mosta fails when any experiment parameters are provided2021-03-23T11:13:30+01:00Alexander Stekelenburgmosta fails when any experiment parameters are providedWhen any experiment parameters are provided to the mosta tool it will complain that no value is specified for one of the model parameters. This happens because the ExperimentInstantiationConversion is added to the TransformationGraph but...When any experiment parameters are provided to the mosta tool it will complain that no value is specified for one of the model parameters. This happens because the ExperimentInstantiationConversion is added to the TransformationGraph but the parameters are not passed to it. This is not an issue when no experiment parameters are given because in that case the ExperimentInstantiationConversion won't be added to the TransformationGraph.https://dgit.cs.uni-saarland.de/modest/toolset/-/issues/94mosta doesn't check if a dotOutputFile is specified when validating the param...2021-03-23T11:23:18+01:00Alexander Stekelenburgmosta doesn't check if a dotOutputFile is specified when validating the parametersCurrently mosta checks whether a dotFormat is specified without an output file which results in an error. It doesn't perform the same check for the dotOutputFile which is also required for the tool to execute without errors. When invoked...Currently mosta checks whether a dotFormat is specified without an output file which results in an error. It doesn't perform the same check for the dotOutputFile which is also required for the tool to execute without errors. When invoked using the command line this isn't a problem because it is impossible to specify a dot format without also providing a dotOutputFile. However when invoking the tool programmatically it is possible to specify these parameters separately.https://dgit.cs.uni-saarland.de/modest/toolset/-/issues/95Missing DisplayNames in DotExporter and PythonExporter2021-03-29T10:37:48+02:00Peter SmitMissing DisplayNames in DotExporter and PythonExporterBoth the Dot- and PythonExporter's parameters classes are missing the DisplayName attribute on their properties.Both the Dot- and PythonExporter's parameters classes are missing the DisplayName attribute on their properties.https://dgit.cs.uni-saarland.de/modest/toolset/-/issues/98Assertion fail when executing mosta2022-03-25T15:02:29+01:00Joost SessinkAssertion fail when executing mostaIf `./modest mosta` is executed using the debug version of Modest, the assertion at line 566 of `CommandLineParser.cs` fails.If `./modest mosta` is executed using the debug version of Modest, the assertion at line 566 of `CommandLineParser.cs` fails.https://dgit.cs.uni-saarland.de/modest/toolset/-/issues/99wlan-large identified as an STA model, PTA expected2022-06-20T17:59:15+02:00Valentijn Holwlan-large identified as an STA model, PTA expectedThe [wlan-large](https://qcomp.org/benchmarks/#wlan-large) benchmark is listed as a PTA model in QComp.
One would expect MCSTA to identify it as such, however it's identified as a STA instead. See output:
```
wlan-large.jani:model: inf...The [wlan-large](https://qcomp.org/benchmarks/#wlan-large) benchmark is listed as a PTA model in QComp.
One would expect MCSTA to identify it as such, however it's identified as a STA instead. See output:
```
wlan-large.jani:model: info: wlan-large is an STA model.
wlan-large.jani: info: Need 16 bytes per state.
...
```https://dgit.cs.uni-saarland.de/modest/toolset/-/issues/100Mec in Interval Iteration2022-09-20T15:11:33+02:00Ivan HopMec in Interval IterationUsing the following command.
check erlang.jani -E K=5000,R=100,TIME_BOUND=50 --alg IntervalIteration --props TminReach
The statespace of interval iterations contains a mec.
State with index 8 goes to state with index 11. The state wit...Using the following command.
check erlang.jani -E K=5000,R=100,TIME_BOUND=50 --alg IntervalIteration --props TminReach
The statespace of interval iterations contains a mec.
State with index 8 goes to state with index 11. The state with index 11 goes to state with index 8. All with one branch and probability one.
I noticed that avoid was null.https://dgit.cs.uni-saarland.de/modest/toolset/-/issues/101Re-enabling location variables and optimisation in Simulation may affect DSMC...2023-02-04T10:08:57+01:00Arnd HartmannsRe-enabling location variables and optimisation in Simulation may affect DSMC/oraclesIn Simulation/SimulationAnalysisEngine.cs, commit b419eb6adcad4bca29871cb122ca72e876f3372a (which merged Michaela's work on resolving nondeterminism via neural networks (DSMC) or external oracles in Simulation) commented out two model tr...In Simulation/SimulationAnalysisEngine.cs, commit b419eb6adcad4bca29871cb122ca72e876f3372a (which merged Michaela's work on resolving nondeterminism via neural networks (DSMC) or external oracles in Simulation) commented out two model transformations:
`//new Guid("14323163-B374-4AEC-976A-49EBDFE9D458"), // detect and expand location variables //commented out to preserve automata edge order from JANI file`
and
`//nstaOptimizationGuid = new Guid("10D9051D-FA26-468F-B138-60F26C729037"), // optimize automata/network //commented out to preserve automata edge order from JANI file`
The former is important for performance, and the latter is important to replace complex constant expressions with their actual numeric values. Especially commenting out the latter is currently leading to errors on QVBS models.
I am now re-enabling these two transformations, but this may have an impact on DSMC/oracles. I ask those who maintain the DSMC/oracle functionality to please review the impact and adapt the DSMC/oracle code accordingly. The first transformation (location variables) could be conditionally disabled when using DSMC/oracles, but the second one (optimisation) is necessary to make several models compile in the first place.https://dgit.cs.uni-saarland.de/modest/toolset/-/issues/102Setting cycle-bound to 0 in modes leads to run length being exceeded immediately2023-02-02T19:21:29+01:00Arnd HartmannsSetting cycle-bound to 0 in modes leads to run length being exceeded immediately...whereas it should lead to unbounded cycle detection....whereas it should lead to unbounded cycle detection.Arnd HartmannsArnd Hartmanns