Exception in mcsta when called on Jani file with two initial states
Hi, when executing a Jani model init2.jani of a racetrack domain 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.b__7_1(KeyValuePair2 kvp) bei System.Linq.Enumerable.WhereSelectEnumerableIterator
2.MoveNext()
bei System.Linq.Enumerable.d__591.MoveNext() bei Modest.Expressions.NormalForms.Implode(IEnumerable
1 expressions, Func3 combine) bei Modest.Expressions.NormalForms.ImplodeCNF(IEnumerable
1 expressions, ILocation defaultLocation)
bei Modest.Automaton.Optimizer.LocalVariableMerger.TransformAutomaton(Automaton automaton)
bei Modest.Automaton.AutomatonTransformer.b__25_0(Automaton automaton)
bei Modest.Automaton.AutomataComposition.Transform(Func2 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, Func2 parameters, OperationState operationState, IErrorHandler errors) bei Modest.ModelChecking.ModelCheckingAnalysisEngine.Analyze(AnalysisParams analysisParameters, NSHAModel model, IEnumerable
1 modelParameters, OperationState operationState, IErrorHandler errors)
bei Modest.Modularity.AnalysisEngine3.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, Michaela