toolset issueshttps://dgit.cs.uni-saarland.de/modest/toolset/-/issues2023-02-02T19:21:29+01:00https://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/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.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/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/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/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/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/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/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/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/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/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/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/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/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
```