toolset issueshttps://dgit.cs.uni-saarland.de/modest/toolset/-/issues2019-03-17T20:17:36+01:00https://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/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/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/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/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/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/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/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/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/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/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/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/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/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/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/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/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/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/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/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.de