toolset issueshttps://dgit.cs.uni-saarland.de/modest/toolset/-/issues2017-12-08T23:29:54+01:00https://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/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/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/32Location names in ToString() representation of states (T: struct)2018-03-07T15:22:40+01:00Michaela Klauckklauck@depend.uni-saarland.deLocation names in ToString() representation of states (T: struct)When trying to step through a compiled network of states (state struct `T`) by printing the visited states using `ToString()`, I noticed that the variables are named as specified in the input model (e.g. in the `Jani`-file), such that th...When trying to step through a compiled network of states (state struct `T`) by printing the visited states using `ToString()`, I noticed that the variables are named as specified in the input model (e.g. in the `Jani`-file), such that the variable-value-mapping can be easily identified (e.g. `counter = 0` for a variable named `counter` introduced in the `Jani`-model). But the locations of the automata are numbered in the order they are specified in the input file and their names are not used in the state representation, such that they can not be recognized directly. For example a declaration of locations:
``"locations": [
{
"name": "loc10",
"transient-values": []
},
...
{
"name": "loc0",
"transient-values": []
},
``
will in the end result in states, where `automaton.location = 0` in the `ToString()` representation indicates that the location is `loc10`, because `loc10` is the first declaration of a location. It would be much more intuitive if the current location in each automaton would be indicated by the location's name (e.g. `automaton.location = loc0`), like it is done for variables.Sanny SchmittSanny Schmitthttps://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/29Remove dependency of motest on Simulation2018-03-01T06:51:19+01:00Arnd HartmannsRemove dependency of motest on SimulationThe motest executable project currently depends on the Simulation project. This is strange, since simulation and model-based testing would appear to be two rather independent things. The reason appears to be that `MotestParams` derives f...The motest executable project currently depends on the Simulation project. This is strange, since simulation and model-based testing would appear to be two rather independent things. The reason appears to be that `MotestParams` derives from `SimulationAnalysisToolchain.AnalysisParams`. I don't think that should be the case; the parameters for model-based testing are clearly not a superset of the parameters for simulation (does model-based testing do e.g. scheduler sampling or rare event simulation?). I suggest removing the dependency of motest on Simulation.Alexander Graf-BrillAlexander Graf-Brillhttps://dgit.cs.uni-saarland.de/modest/toolset/-/issues/27Properties should not be part of an automata network2017-12-07T12:04:40+01:00Gereon Foxgfox@mpi-inf.mpg.deProperties should not be part of an automata networkThis is a rather philosophical issue, and it is a humble test baloon. On a meta-level, I am posting it to find out how people react to it and whether we care about these kinds of questions at all:
Today I noticed again that **in order t...This is a rather philosophical issue, and it is a humble test baloon. On a meta-level, I am posting it to find out how people react to it and whether we care about these kinds of questions at all:
Today I noticed again that **in order to construct an automata network, you have to give properties**, i.e. the AutomataNetwork class forces you to pass it a set of properties when an automata network is to be created. This in itself is IMHO already bad design because in the mental concept of a network of automata, properties are just absent: It is perfectly natural to think of an automata network without ever bothering about the concept of property at all.
However, I also have two more technical arguments to support my point:
1. If you construct an automata network, but don't know the properties to check yet, you will later have to create a copy of the network with those properties as an argument to the constructor. I find this counter-intuitive and - at least in theory - wasteful. I would rather expect the model checker to take two completely separate arguments, i.e. the automata network and then a set of properties that are defined over the set of variables one finds in that network.
2. The fact that the type `Property` occurs in the definition of the type `AutomataNetwork` creates a tight coupling between those types. I think that in general one rather strives towards *loose* coupling because reducing dependencies among different parts of the code makes it easier to maintain and easier to reuse for a new purpose (which people like Michaela, Gregory, or myself are doing as their primary task).
I can imagine that despite the above counter-arguments, this design might have been chosen because it allows an easier interface to the model checker (which thus has to take only one single argument, and not several), but because of those counter-arguments, I would like to overhaul it.
In case the feedback for this suggestion of mine is positive, I intend to do two things:
1. Find out whether resolving this issue is indeed worth the gain and then have Sanny resolve it.
2. Keep an eye open for and collect more issues of this kind. I have a feeling that they occur in a number of places, but so far I never took care to remember them. However I just realized that often when Gregory or Michaela ask me for help and also when I myself am struggling, problems are at least partly connected to tight coupling (may it be actual or perceived). I therefor consider tight coupling a technical debt that you're sometimes willing to make, but that we're paying quite some interest on. So let's pay back some of it.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/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/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 Hartmannshttps://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/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/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/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/97export-to-dot not working in v3.1.105-gbac8737902021-09-14T21:40:22+02:00Ivan Hopexport-to-dot not working in v3.1.105-gbac873790Using export=to-dot gives a crash with v3.1.105-gbac873790. I am using windows. Using v3.1.76-gfc18cd82b (previous version installed) it worked.
![crash](/uploads/e57ca5ba3dca7cf671ff0b46536cfdc3/crash.png)Using export=to-dot gives a crash with v3.1.105-gbac873790. I am using windows. Using v3.1.76-gfc18cd82b (previous version installed) it worked.
![crash](/uploads/e57ca5ba3dca7cf671ff0b46536cfdc3/crash.png)https://dgit.cs.uni-saarland.de/modest/toolset/-/issues/96segmentation fault - calling function from if statement2021-09-14T21:40:47+02:00Jonah Boesegmentation fault - calling function from if statementIn the following code segment, creating variable _flit_ is the only way I've found to run this code without errors. Removing _flit_ and replacing all occurrences with _peekFront(noc[id].channels[LOCAL].buffer_ causes the error:
zsh: segm...In the following code segment, creating variable _flit_ is the only way I've found to run this code without errors. Removing _flit_ and replacing all occurrences with _peekFront(noc[id].channels[LOCAL].buffer_ causes the error:
zsh: segmentation fault modest check 3-receive-send.modest
```
// Advance flits to respective buffers
process AdvanceFlits(int id){
// If flit needs to stay on this row
// TODO fix for x-y routing
int flit;
{=
flit = peekFront(noc[id].channels[LOCAL].buffer)
=};
if(flit >= getFirstInRow(id) && flit <= getLastInRow(id)){
// Send it west
if(flit < id){
Send(id, LOCAL, WEST)
}
// Or send it east
else{
Send(id, LOCAL, EAST)
}
}
// Else, if flit needs to go north
else if(flit < id){
Send(id, LOCAL, NORTH)
}
// Else, flit needs to go south
else{
Send(id, LOCAL, SOUTH)
}
}
```
Here is the entire model:
[3-receive-send.modest](/uploads/c00f29d2eb825e62079aba37a9b52542/3-receive-send.modest)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/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.