Interval 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_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))...