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/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.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/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 Hartmanns