Skip to content

Exceptions when excecuting prohver

Running prohver with the current version on the master branch results in an uncaught ArgumentNullException with any hybrid model.

Error message: An unhandled exception of type 'System.ArgumentNullException' occurred in System.Private.CoreLib.dll: 'Value cannot be null.'

Stack Trace:

  • at System.ArgumentNullException.Throw(String paramName)
  • at System.ArgumentNullException.ThrowIfNull(Object argument, String paramName)
  • at Modest.Exploration.Compiled.CompiledState..ctor(CompiledAutomata compiledAutomata, AutomataNetwork network, ExplorationConfiguration config, Dictionary`2 clockBounds, StateProjection[] projections) in /home/annabell/src/toolset/Exploration/Compiled/CompiledState.cs:line 269
  • at Modest.Exploration.Compiled.NetworkCompiler.CompileStateType(AutomataNetwork network, CompiledAutomata ca, ExplorationConfiguration config, Dictionary`2 clockBounds, StateProjection[] projections) in /home/annabell/src/toolset/Exploration/Compiled/NetworkCompiler.cs:line 60
  • at Modest.Exploration.NetworkCompilerHelper.Compile(AutomataNetwork automataNetwork, ExplorationConfiguration config, Expression[] expressions, Expression[] timeConstraints, Dictionary`2 clockBounds, StateProjection[] projections, OperationState operationState, String extraStatusString) in /home/annabell/src/toolset/Exploration/Compiled/NetworkCompilerHelper.cs:line 22
  • at Modest.Hybrid.SymbolicAutomaton.FromAutomataNetwork(AutomataNetwork automataNetwork, Expression[] expressions, OperationState operationState, ComponentErrorHandler ceh) in /home/annabell/src/toolset/Hybrid/SymbolicAutomatonBuilder.cs:line 26
  • at Modest.Hybrid.PhaverAnalysisEngine.Analyze(AnalysisParams analysisParameters, NSHAModel model, OperationState operationState, IErrorHandler errors) in /home/annabell/src/toolset/Hybrid/PHAVer/PhaverAnalysisEngine.cs:line 664
  • at Modest.Hybrid.PhaverAnalysisEngine.Analyze(AnalysisParams analysisParams, NSHAModel model, Int32 index, Boolean isLast, IExperiment[] modelParameters, OperationState operationState, IErrorHandler errors) in /home/annabell/src/toolset/Hybrid/PHAVer/PhaverAnalysisEngine.cs:line 460 -at Modest.Modularity.AnalysisEngine`2.Analyze(IParameterObject analysisParameters, IModel[] models, IExperiment[][] experiments, OperationState operationState, IErrorHandler errors) in /home/annabell/src/toolset/Modularity/Analysis/AnalysisEngine.cs:line 136 -at Modest.Executable.Prohver.Run(IParameterObject parameterObj, Stopwatch time, IOutputHandler outputHandler, CancellationToken cancellationToken) in /home/annabell/src/toolset/modest/Prohver.cs:line 427 -at Modest.Executable.Program.Main(String[] args) in /home/annabell/src/toolset/modest/Program.cs:line 193

The changes in that commit (https://dgit.cs.uni-saarland.de/modest/toolset/-/commit/e794830e9c29c2bc1ba6a11cacde8f100b643e7a) might have caused that issue (see class CompiledState.cs, line 269 added).

When reverting to a previous commit (master): a72d2b6fd and using dotnet 6, the following exception is thrown:

An unhandled exception of type 'System.NullReferenceException' occurred in Modest.ModelChecking.dll: 'Object reference not set to an instance of an object.' - at Modest.ModelChecking.ValueIteration.Multiply(Int64 transitionIndex, Transition* transitions, Branch* branches, Double* probabilities, Double* branchRewards, Double* values, Double* boundRewards, Double* oldValueQueues, Int64* oldValueOffsets, Double& vTrans) in /home/annabell/src/toolset/ModelChecking/ValueIteration.cs:line 967 - at Modest.ModelChecking.ValueIteration.PerformUnboundedValueIteration(PropertyAnalysisTask task, Partition partition, Int32 boundValue, LocationErrorHandler leh, CancellationToken ct, Boolean reportCancellation, Int64& iterationCount, Double& error, Boolean& aborted) in /home/annabell/src/toolset/ModelChecking/ValueIteration.cs:line 874 - at Modest.ModelChecking.ValueIteration.PerformPartitionUnboundedValueIteration(PropertyAnalysisTask task, Partition partition, Int64 iteration, UnboundedValueIterationPartitionData data, String statusFormat, LocationErrorHandler leh, OperationState stepOperationState) in /home/annabell/src/toolset/ModelChecking/ValueIteration.cs:line 656 - at Modest.ModelChecking.ValueIteration.<>c__DisplayClass7_1.g__FixpointStep|1(Int32 partitionIndex, Int32 iteration, OperationState stepOperationState) in /home/annabell/src/toolset/ModelChecking/ValueIteration.cs:line 209 - at Modest.StateSpace.Helpers.IteratePartitions(StateSpace stateSpace, Action`2 preProcess, Func`4 fixpointStep, Action`2 postProcess, OperationState operationState) in /home/annabell/src/toolset/StateSpace/Helpers.cs:line 88 - at Modest.ModelChecking.ValueIteration.IterateUnbounded(PropertyAnalysisTask task, StateSpace stateSpace, AnalysisDataSet dataSet, String statusFormat, LocationErrorHandler leh, OperationState operationState) in /home/annabell/src/toolset/ModelChecking/ValueIteration.cs:line 218 - at Modest.Hybrid.PhaverAnalysisEngine.InvokePhaverAndCalculateProbability(SymbolicAutomaton symbolicAutomaton, PhaverProperty property, PhaverOutputConfiguration config, String phaverPath, PropertyAnalysisTask task, String statusExperimentString, FileInfo outputModelFile, Boolean overwriteOutputModelFile, FileInfo inputGraphFile, ILocation documentLocation, OperationState operationState, ComponentErrorHandler ceh) in /home/annabell/src/toolset/Hybrid/PHAVer/PhaverAnalysisEngine.cs:line 897 - at Modest.Hybrid.PhaverAnalysisEngine.Analyze(AnalysisParams analysisParameters, NSHAModel model, OperationState operationState, IErrorHandler errors) in /home/annabell/src/toolset/Hybrid/PHAVer/PhaverAnalysisEngine.cs:line 695 - at Modest.Hybrid.PhaverAnalysisEngine.Analyze(AnalysisParams analysisParams, NSHAModel model, Int32 index, Boolean isLast, IExperiment[] modelParameters, OperationState operationState, IErrorHandler errors) in /home/annabell/src/toolset/Hybrid/PHAVer/PhaverAnalysisEngine.cs:line 460