toolset issueshttps://dgit.cs.uni-saarland.de/modest/toolset/-/issues2021-03-23T11:13:30+01:00https://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/92Digital Clock conversion crashes2021-03-05T14:49:49+01:00Bram KohlenDigital Clock conversion crashesIn the latest version of Modest that is downloadable from the site I get a Stack Overflow when performing the digital clocks conversion. I have used the bip-pta.v1.modest from https://qcomp.org/benchmarks/#brp-pta and I used the command ...In the latest version of Modest that is downloadable from the site I get a Stack Overflow when performing the digital clocks conversion. I have used the bip-pta.v1.modest from https://qcomp.org/benchmarks/#brp-pta and I used the command moconv {PATH TO}/brp-pta.v1.modest -O {PATH_TO}/brp-pta.v1.jani --digital-clocks. This results in a Stack Overflow. If I run the same command without digital clocks conversion (i.e. moconv {PATH TO}/brp-pta.v1.modest -O {PATH_TO}/brp-pta.v1.jani) then it does not crash.
I did some debugging and I found that the error was caused by an "if" statement that was changed to an "else if" statement in Expressions/Optimizer.cs in Line 528. Changing this back to "if" again resolves the issue.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/89Exception in mcsta when called on Jani file with two initial states2019-11-07T17:28:36+01:00Michaela Klauckklauck@depend.uni-saarland.deException in mcsta when called on Jani file with two initial statesHi,
when executing a Jani model [init2.jani](/uploads/4e18d64f6ef6afecc88c108d5cbae44a/init2.jani) of a racetrack domain [init2.track](/uploads/740e3b40e44a2afa610c0443429a3f2e/init2.track) with two initial states we get this error messa...Hi,
when executing a Jani model [init2.jani](/uploads/4e18d64f6ef6afecc88c108d5cbae44a/init2.jani) of a racetrack domain [init2.track](/uploads/740e3b40e44a2afa610c0443429a3f2e/init2.track) with two initial states we get this error message:
`init2.jani:model: info: racetrack is an MDP model.
Unbehandelte Ausnahme: System.NullReferenceException: Der Objektverweis wurde nicht auf eine Objektinstanz festgelegt.
bei Modest.Automaton.Optimizer.LocalVariableMerger.<>c.<TransformAutomaton>b__7_1(KeyValuePair`2 kvp)
bei System.Linq.Enumerable.WhereSelectEnumerableIterator`2.MoveNext()
bei System.Linq.Enumerable.<ConcatIterator>d__59`1.MoveNext()
bei Modest.Expressions.NormalForms.Implode(IEnumerable`1 expressions, Func`3 combine)
bei Modest.Expressions.NormalForms.ImplodeCNF(IEnumerable`1 expressions, ILocation defaultLocation)
bei Modest.Automaton.Optimizer.LocalVariableMerger.TransformAutomaton(Automaton automaton)
bei Modest.Automaton.AutomatonTransformer.<TransformComposition>b__25_0(Automaton automaton)
bei Modest.Automaton.AutomataComposition.Transform(Func`2 transformer, OperationState operationState)
bei Modest.Automaton.AutomatonTransformer.TransformNetwork(AutomataNetwork network)
bei Modest.Automaton.AutomatonTransformer.Transform(AutomataNetwork network)
bei Modest.Automaton.Optimizer.Optimize(AutomataNetwork network, Boolean optimizeVariables, Boolean optimizeLocations, Boolean optimiseInputEnabledness, Boolean optimiseAssignmentIndices)
bei Modest.Automaton.NSHAOptimizationConversion.Convert(ConversionParams conversionParams, NSHAModel nstaModel, OperationState operationState, IErrorHandler errors)
bei Modest.Modularity.ModelConversion`2.Convert(IParameterObject conversionParameters, IModel source, OperationState operationState, IErrorHandler errors)
bei Modest.Modularity.TransformationGraphExtensions.ConvertChecked(IModelConversion modelConversion, IParameterObject parameters, IModel[] input, OperationState operationState, IErrorHandler errors)
bei Modest.Modularity.TransformationGraph.Execute(IModel[] models, Func`2 parameters, OperationState operationState, IErrorHandler errors)
bei Modest.ModelChecking.ModelCheckingAnalysisEngine.Analyze(AnalysisParams analysisParameters, NSHAModel model, IEnumerable`1 modelParameters, OperationState operationState, IErrorHandler errors)
bei Modest.Modularity.AnalysisEngine`3.Analyze(IParameterObject analysisParameters, IModel model, IEnumerable`1 experiments, OperationState operationState, IErrorHandler errors)
bei Modest.Executables.Mcsta.Program.Run(McstaParams parameters, Stopwatch time)
bei Modest.Executables.Mcsta.Program.Main(String[] args)`
We know that mcsta and modes are not able to handle models with multiple initial states. But in this case the error message should be something like "complex initial state specifications are not supported". So there must be another problem, either in the Jani file or in Modest. We generated the Jani file from a file representing the map in ASCII using a python script. Models with only one initial state are translated correctly.
Thank you very much for your help!
Best,
Michaelahttps://dgit.cs.uni-saarland.de/modest/toolset/-/issues/88BEB confluence case study model does not contain run parameters2019-07-08T12:04:22+02:00Hans van der LaanBEB confluence case study model does not contain run parametersThe beb.confluence.modest model in the Case Study folder is missing the command line arguments an user should use to run the model as intended in mcsta/modes.
It seems as if we should just give the same arguments as provided with the b...The beb.confluence.modest model in the Case Study folder is missing the command line arguments an user should use to run the model as intended in mcsta/modes.
It seems as if we should just give the same arguments as provided with the beb.modest model. However, I am not sure what the confluence resolver is and if any additional parameters could/should be used.https://dgit.cs.uni-saarland.de/modest/toolset/-/issues/87Unsupported property warning gives no indication why the property is unsupported2019-07-08T12:06:14+02:00Hans van der LaanUnsupported property warning gives no indication why the property is unsupportedWhen testing the Sound Value Iteration algorithm on models from QCOMP, I get the warning that the properties 'danger_T', 'down_T' and 'up_T' from the [Embedded Control System Model](http://qcomp.org/benchmarks/index.html#embedded) are un...When testing the Sound Value Iteration algorithm on models from QCOMP, I get the warning that the properties 'danger_T', 'down_T' and 'up_T' from the [Embedded Control System Model](http://qcomp.org/benchmarks/index.html#embedded) are unsupported.
```
embedded.jani:properties[2]: warning: Skipping unsupported property "danger_T".
embedded.jani:properties[4]: warning: Skipping unsupported property "down_T".
embedded.jani:properties[12]: warning: Skipping unsupported property "up_T".
```
From these warning messages, as user I have no idea why these properties are currently unsupported. Is this because they contain nested PCTL (and thus will be supported when we finish merging the nested PCTL feature branch) or do these properties contain any other special feature which we currently do not support?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/84Precision bug, rounding error in int/real mixed expressions2019-08-12T12:14:19+02:00Michaela Klauckklauck@depend.uni-saarland.dePrecision bug, rounding error in int/real mixed expressionsHi,
Marcel Steinmetz (@steinmetz) and me are working on a Jani model of the race track domain. In Modest the positions in the grid are not calculated correctly. We suppose that there is a precision bug, a rounding error or a problem wit...Hi,
Marcel Steinmetz (@steinmetz) and me are working on a Jani model of the race track domain. In Modest the positions in the grid are not calculated correctly. We suppose that there is a precision bug, a rounding error or a problem with mixed int/real expressions. The critical action seems to be around line 455 in this file: [rt.jani](/uploads/8a0f91a0b4cf1580ed1cd50a4491ee34/rt.jani). All varaibles involved in the calculations are integers and the result should again be an integer. In our case the result for one of the coordinates is -2 instead of -1. To make sure that the problem is not caused by a modelling error in the Jani file, we removed the 2D arrays not supported by Storm and hardcoded these information. In this case Storm returns the correct results.
If needed, we can try to find a minimal example where this error occurs but we are not sure how large this will be. The domain represented in the file above looks like this:
`dimensions: 1 3 `
`start empty_location goal`
Best,
Michaelahttps://dgit.cs.uni-saarland.de/modest/toolset/-/issues/83Interval Iteration crashes because end component file already exists2019-05-21T14:18:36+02:00Hans van der LaanInterval Iteration crashes because end component file already exists**Problem:**
When we try to check the BRP model from the case studies with interval iteration, mcsta crashes.
**Input:**
```
..\Modest\mcsta.exe ".\rewards\testcases\brp.modest" --alg IntervalIteration -E "N=16, MAX=2, TD=1, TIME_BOUN...**Problem:**
When we try to check the BRP model from the case studies with interval iteration, mcsta crashes.
**Input:**
```
..\Modest\mcsta.exe ".\rewards\testcases\brp.modest" --alg IntervalIteration -E "N=16, MAX=2, TD=1, TIME_BOUND=64"
```
**Output:**
```
PS C:\Users\Gebruiker\Documents\Werk\Modest\Workspace> ..\Modest\mcsta.exe ".\rewards\testcases\brp.modest" --alg IntervalIteration -E "N=16, MAX=2, TD=1, TIME_BOUND=64"
(00:00) 0.....
Preparing model checking...
brp.modest: info: brp is a PTA model.
(00:01) 0.............
Compiling model for N=16, MAX=2, TD=1, TIME_BOUND=64...
brp.modest: info: Need 40 bytes per state.
(00:01) 0...................10....
State-space exploration for N=16, MAX=2, TD=1, TIME_BOUND=64 (cleanup)...
brp.modest: info: Explored 3959 states for N=16, MAX=2, TD=1, TIME_BOUND=64.
(00:01) 0...................10...................20...................30...................40...................50..........
Checking property "P_1" for N=16, MAX=2, TD=1, TIME_BOUND=64 (end components (iteration 2))...
brp.modest: info: Identified 2158 maximal end components.
(00:01) 0...................10...................20...................30...................40...................50...................60.
Checking property "P_2" for N=16, MAX=2, TD=1, TIME_BOUND=64 (end components (iteration 2))...
brp.modest: info: Identified 1697 maximal end components.
Unhandled Exception: System.IO.IOException: The file 'C:\Users\Gebruiker\AppData\Local\Temp\d40cb6d6bc0348bc920b13d823ec6ec9\States (merged end components).bin' already exists.
at System.IO.__Error.WinIOError(Int32 errorCode, String maybeFullPath)
at System.IO.FileStream.Init(String path, FileMode mode, FileAccess access, Int32 rights, Boolean useRights, FileShare share, Int32 bufferSize, FileOptions options, SECURITY_ATTRIBUTES secAttrs, String msgPath, Boolean
bFromProxy, Boolean useLongPath, Boolean checkHost)
at System.IO.FileStream..ctor(String path, FileMode mode, FileSystemRights rights, FileShare share, Int32 bufferSize, FileOptions options)
at System.IO.MemoryMappedFiles.MemoryMappedFile.CreateFromFile(String path, FileMode mode, String mapName, Int64 capacity, MemoryMappedFileAccess access)
at Modest.StateSpace.Memory..ctor(Int64 length, String path, FileMode fileMode, Boolean zeroMemory, Boolean deleteOnDispose)
at Modest.StateSpace.StateSpace..ctor(DirectoryInfo folder, String suffix, Int64 stateCount, Int32 atomicPropositionCount, Int64 transitionCount, Int64 branchCount, Int32 rewardCount)
at Modest.ModelChecking.EndComponents.CollapseEndComponents(PropertyAnalysisTask task, StateSpace stateSpace, AnalysisDataSet dataSet, String statusFormat, LocationErrorHandler leh, OperationState operationState)
at Modest.ModelChecking.MAModelChecker`1.CheckProperty(StateSpace stateSpace, ReachabilityPropertyInfo prop, String avoidStatesKey, String targetStatesKey, StateSet`1 stateSet, IDisposable& previousBoundedIterationInfo, Func`3 onProbabilityNotZeroOrOne, String propertyStatusString, AnalysisDataSet info, OperationState operationState, ComponentErrorHandler ceh)
at Modest.ModelChecking.MAModelChecker`1.ModelCheck(String experimentString, OperationState operationState, ComponentErrorHandler ceh)
at Modest.ModelChecking.ModelCheckingAnalysisEngine.ModelCheckGeneric[T](Network`1 network, Object expInfoObj, String experimentString, StateProjections projections, Object propertiesObj, ComponentisedExpression[] distanceExps, Object parametersObj, ILocation documentLocation, OperationState operationState, ComponentErrorHandler ceh)
at invoke Modest.Exploration.Network`1__CompiledAutomata.State1\, CompiledAutomata2286545746817054944\, 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(Object , Object[] , MethodInfo )
at Modest.DirectInvoker.InvokeDirect(MethodInfo method, Object instance, Object[] parameters)
at Modest.ModelChecking.ModelCheckingAnalysisEngine.ModelCheck(NSHAModel model, CompilationParameters compilationParams, Object parametersObj, OperationState operationState, IErrorHandler errors)
at Modest.ModelChecking.ModelCheckingAnalysisEngine.Analyze(AnalysisParams analysisParameters, NSHAModel model, IEnumerable`1 modelParameters, OperationState operationState, IErrorHandler errors)
at Modest.Modularity.AnalysisEngine`3.Analyze(IParameterObject analysisParameters, IModel model, IEnumerable`1 experiments, OperationState operationState, IErrorHandler errors)
at Modest.Executables.Mcsta.Program.Run(McstaParams parameters, Stopwatch time)
at Modest.Executables.Mcsta.Program.Main(String[] args)
(00:05) 0...................10...................20...................30...................40...................50...................60..
Checking property "P_2" for N=16, MAX=2, TD=1, TIME_BOUND=64 (end components (merging))...
```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/80Turn off optimization(s) in mcsta2020-02-11T13:08:00+01:00Hans van der LaanTurn off optimization(s) in mcstaAs discussed, #78 was not a real bug but actually the consequence of an optimization. It's reasonable to expect the user might want to visualize an unoptimized version. We should add a parameter to turn off certain/all optimizations in m...As discussed, #78 was not a real bug but actually the consequence of an optimization. It's reasonable to expect the user might want to visualize an unoptimized version. We should add a parameter to turn off certain/all optimizations in mcsta.https://dgit.cs.uni-saarland.de/modest/toolset/-/issues/79Interval Iteration does not converge for large Haddad-Monmege example2019-11-07T17:29:46+01:00Hans van der LaanInterval Iteration does not converge for large Haddad-Monmege example**Problem:**
The interval iteration algorithm does not converge on the 2nd haddad monmege example from QComp. It seems as the width says stuck at 0.5.
**Parameters:**
```
".\haddad-monmege.jani" --alg IntervalIteration -E "N = 100, p =...**Problem:**
The interval iteration algorithm does not converge on the 2nd haddad monmege example from QComp. It seems as the width says stuck at 0.5.
**Parameters:**
```
".\haddad-monmege.jani" --alg IntervalIteration -E "N = 100, p = 0.7"
```Hans van der LaanHans van der Laanhttps://dgit.cs.uni-saarland.de/modest/toolset/-/issues/78Statespace contains unreachable states2020-02-10T18:38:54+01:00Hans van der LaanStatespace contains unreachable states**Problem:**
In the following example, state should always be equal to global_state. However, the export shows this is not always the case. Interestingly, the problem dissapears when we move the safe and risk action from after the weight...**Problem:**
In the following example, state should always be equal to global_state. However, the export shows this is not always the case. Interestingly, the problem dissapears when we move the safe and risk action from after the weights to before the palt,
**Code:**
```
action start, safe, risk, finish, close, reset;
int global_state = 0;
property p1 = Pmax(<> (global_state == 2));
process Server(int state)
{
alt {
:: when(state == 0) start {= state = 1, global_state = 1 =}
:: when(state == 1) alt {
:: palt {
:6: safe {= state = 0, global_state = 0 =}
:3: safe {= state = 2, global_state = 2 =}
:1: safe {= state = 3, global_state = 3 =}
}
:: palt {
:5: risk {= state = 2, global_state = 2 =}
:5: risk {= state = 3, global_state = 3 =}
}
}
:: when(state == 2) finish {= state = 2, global_state = 2 =}
:: when(state == 3)
alt {
:: close {= state = 3, global_state = 3 =}
:: reset {= state = 0, global_state = 0 =}
}
};
Server(state)
}
Server(0)
```
**Image:**
![image](/uploads/76fea69dfdecc75dd9fda1cffa1adc26/image.png)
**Code 2:**
```
action start, safe, risk, finish, close, reset;
int global_state = 0;
property p1 = Pmax(<> (global_state == 2));
process Server(int state)
{
alt {
:: when(state == 0) start {= state = 1, global_state = 1 =}
:: when(state == 1) alt {
:: safe palt {
:6: {= state = 0, global_state = 0 =}
:3: {= state = 2, global_state = 2 =}
:1: {= state = 3, global_state = 3 =}
}
:: risk palt {
:5: {= state = 2, global_state = 2 =}
:5: {= state = 3, global_state = 3 =}
}
}
:: when(state == 2) finish {= state = 2, global_state = 2 =}
:: when(state == 3)
alt {
:: close {= state = 3, global_state = 3 =}
:: reset {= state = 0, global_state = 0 =}
}
};
Server(state)
}
Server(0)
```
**Image 2:**
![image](/uploads/ceffcfc18972ef95af44dec912a487d0/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/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"```.