[mcsta] NullReferenceException with option "chainopt"
mcsta
crashes on this small model when I pass the --chainopt
option.
clock c;
bool success;
property P = Pmin(<> success);
invariant (c <= 5)
when (c == 5)
tau {= success = true =}
I call mcsta
via mono mcsta.exe --chainopt model.modest
.
I get the following stacktrace:
[ERROR] FATAL UNHANDLED EXCEPTION: System.NullReferenceException: Object reference not set to an instance of an object
at Modest.StateSpace.StateSpaceExploration`1[T].ExploreStateSpacePartition (Modest.Exploration.Network`1[T] network, Modest.StateSpace.StateSpace stateSpace, System.Int32 partitionIndex, Modest.StateSpace.StateSpaceExploration`1+StatePartitionIndexGetter[T] getPartition, Modest.StateSpace.StateSpaceExploration`1+StateDataGetter[T] getStateData, System.Int32[] rewardExpressions, Modest.StateSpace.StateSpaceExploration`1+TransitionHandler[T] handleTransition, System.UInt64 terminalStates, System.Collections.Generic.Dictionary`2[TKey,TValue] partitionStates, System.Collections.Generic.List`1[T] partitionDone, Modest.StateSpace.StateSpaceExploration+Configuration configuration, Modest.StateSpace.StateSpaceExploration+Diagnostics diagnostics, Modest.StateSpace.StateSpaceExploration`1+StatusCallbackData[T] statusData, Modest.Modularity.OperationState operationState) [0x00629] in <af3ca1b51aa04b84a423a384f78db6c5>:0
at Modest.StateSpace.StateSpaceExploration`1[T].ExploreStateSpace (Modest.Exploration.Network`1[T] network, Modest.StateSpace.StateSpaceExploration`1+StatePartitionGetter[T] getStatePartition, Modest.StateSpace.StateSpaceExploration`1+StateDataGetter[T] getStateData, System.Int32 rewardExpressionsOffset, System.Int32 rewardExpressionsCount, Modest.StateSpace.StateSpaceExploration`1+TransitionHandler[T] handleTransition, System.UInt64 terminalStates, Modest.StateSpace.StateSpaceExploration+Configuration configuration, Modest.StateSpace.StateSpaceExploration+Diagnostics diagnostics, System.String experimentString, Modest.Modularity.OperationState operationState) [0x00244] in <af3ca1b51aa04b84a423a384f78db6c5>:0
at Modest.ModelChecking.MDPModelChecker`1+StateSpaceExplorer[T].ExploreStateSpace (Modest.StateSpace.StateSpaceExploration+Diagnostics diagnostics, System.Boolean collectDiagnostics, System.String experimentString, Modest.Modularity.OperationState operationState) [0x00089] in <131a9aa533a44f5497bff16ab0e6cde7>:0
at Modest.ModelChecking.MDPModelChecker`1[T].ModelCheck (System.String experimentString, Modest.Modularity.OperationState operationState, Modest.Modularity.ComponentErrorHandler ceh) [0x001cd] in <131a9aa533a44f5497bff16ab0e6cde7>:0
at Modest.ModelChecking.ModelCheckingAnalysisEngine.ModelCheckGeneric[T] (Modest.Exploration.Network`1[T] network, Modest.ModelChecking.MDPModelChecker+ExpressionsInfo expInfo, System.String experimentString, System.Object propertiesObj, System.Object parametersObj, Modest.Modularity.ILocation documentLocation, Modest.Modularity.OperationState operationState, Modest.Modularity.ComponentErrorHandler ceh) [0x000ac] in <131a9aa533a44f5497bff16ab0e6cde7>:0
at (wrapper delegate-invoke) type_16777215:invoke_AnalysisDataSet_Network`1<State1>_MDPModelChecker/ExpressionsInfo_string_object_object_ILocation_OperationState_ComponentErrorHandler (Modest.Exploration.Network`1<CompiledAutomata.State1>,Modest.ModelChecking.MDPModelChecker/ExpressionsInfo,string,object,object,Modest.Modularity.ILocation,Modest.Modularity.OperationState,Modest.Modularity.ComponentErrorHandler)
at invoke Modest.Exploration.Network`1__CompiledAutomata.State1\, CompiledAutomata10055338152368458001\, Version=0.0.0.0\, Culture=neutral\, PublicKeyToken=null__ : Modest.ModelChecking.MDPModelChecker\+ExpressionsInfo : System.String : System.Object : 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 <ffee3e6e52fe434690015585e82e9bfa>:0
at Modest.DirectInvoker.InvokeDirect (System.Reflection.MethodInfo method, System.Object instance, System.Object[] parameters) [0x00189] in <e82c928a42a84eec8154ba224efa372e>:0
at Modest.Exploration.NetworkGenericMethod.Invoke (System.Object network) [0x00021] in <c4581a3194314979a43dbc5322b322e0>:0
at Modest.ModelChecking.ModelCheckingAnalysisEngine.ModelCheck (Modest.Automaton.NSHAModel model, Modest.ModelChecking.MDPModelChecker+Parameters parameters, Modest.Modularity.OperationState operationState, Modest.Modularity.IErrorHandler errors, Modest.Modularity.ComponentErrorHandler ceh) [0x004b0] in <131a9aa533a44f5497bff16ab0e6cde7>: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) [0x00241] in <131a9aa533a44f5497bff16ab0e6cde7>: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) [0x00170] in <1a7ceb6295254f0f93a3b98ac51bbfd2>:0
at Modest.ModelChecking.ModelCheckingAnalysisToolchain.Analyze (Modest.ModelChecking.ModelCheckingAnalysisToolchain+AnalysisParams analysisParams, Modest.Modularity.IModel model, System.Collections.Generic.IEnumerable`1[T] modelParameters, Modest.Modularity.OperationState operationState, Modest.Modularity.IErrorHandler errors) [0x00307] in <131a9aa533a44f5497bff16ab0e6cde7>:0
at Modest.Modularity.AnalysisToolchain`1[AP].Analyze (Modest.Modularity.IParameterObject analysisParameters, Modest.Modularity.IModel model, System.Collections.Generic.IEnumerable`1[T] modelParameters, Modest.Modularity.OperationState operationState, Modest.Modularity.IErrorHandler errors) [0x000ed] in <1a7ceb6295254f0f93a3b98ac51bbfd2>:0
at Modest.Executables.Mcsta.Program.AnalyseModel (Modest.Modularity.IModel model, Modest.Executables.Mcsta.Program+McstaParams parameters, Modest.Modularity.OperationState operationState, Modest.Modularity.IErrorHandler errors) [0x0008e] in <8be1e155eaee4579a0460a7d165c99f9>:0
at Modest.Executables.Mcsta.Program.Run (Modest.Executables.Mcsta.Program+McstaParams parameters) [0x001db] in <8be1e155eaee4579a0460a7d165c99f9>:0
at Modest.Executables.Mcsta.Program.Main (System.String[] args) [0x00074] in <8be1e155eaee4579a0460a7d165c99f9>:0