From 18a5e44c56fc879bf0f9f4357adccaf87d54cc05 Mon Sep 17 00:00:00 2001 From: Axel Habermaier Date: Mon, 11 Jul 2016 12:21:20 +0200 Subject: [PATCH] cleaned up LtsMin integration; moved ChoiceResolver handling out of RuntimeModel --- Source/LtsMin/LtsMin.cpp | 12 +-- Source/SafetySharp/Analysis/CounterExample.cs | 32 +++---- .../ActivationMinimalExecutedModel.cs | 28 +++---- .../Analysis/ModelChecking/ExecutedModel.cs | 21 +++-- .../Analysis/ModelChecking/StateGraph.cs | 1 - Source/SafetySharp/Analysis/Simulator.cs | 42 +++++----- Source/SafetySharp/Runtime/ChoiceResolver.cs | 10 +-- Source/SafetySharp/Runtime/RuntimeModel.cs | 83 +++++-------------- 8 files changed, 98 insertions(+), 131 deletions(-) diff --git a/Source/LtsMin/LtsMin.cpp b/Source/LtsMin/LtsMin.cpp index 7a56b752..2ff8b320 100644 --- a/Source/LtsMin/LtsMin.cpp +++ b/Source/LtsMin/LtsMin.cpp @@ -97,6 +97,7 @@ ref struct Globals { static ActivationMinimalExecutedModel^ ExecutedModel; static RuntimeModel^ RuntimeModel; + static const char* ModelFile; }; //--------------------------------------------------------------------------------------------------------------------------- @@ -115,18 +116,19 @@ void PrepareLoadModel(model_t model, const char* modelFile) LoadModel(model, modelFile); } +RuntimeModel^ CreateModel() +{ + return Globals::RuntimeModel; +} + void LoadModel(model_t model, const char* modelFile) { try { auto modelData = RuntimeModelSerializer::LoadSerializedData(File::ReadAllBytes(gcnew String(modelFile))); Globals::RuntimeModel = gcnew RuntimeModel(modelData, sizeof(int32_t)); - Globals::ExecutedModel = gcnew ActivationMinimalExecutedModel(Globals::RuntimeModel, 1 << 16); + Globals::ExecutedModel = gcnew ActivationMinimalExecutedModel(gcnew Func(&CreateModel), gcnew array^>(0), 1 << 16); -#if false - Console::WriteLine(Globals::Model->StateVectorLayout); -#endif - auto stateSlotCount = (int32_t)(Globals::RuntimeModel->StateVectorSize / sizeof(int32_t)); auto stateLabelCount = Globals::RuntimeModel->StateFormulas->Length; auto transitionGroupCount = 1; diff --git a/Source/SafetySharp/Analysis/CounterExample.cs b/Source/SafetySharp/Analysis/CounterExample.cs index 58d693f0..a94db0e7 100644 --- a/Source/SafetySharp/Analysis/CounterExample.cs +++ b/Source/SafetySharp/Analysis/CounterExample.cs @@ -119,26 +119,28 @@ public unsafe ModelBase DeserializeState(int position) } /// - /// Gets the replay information for the state identified by the zero-based . + /// Replays the transition of the counter example with the zero-baesd . /// - /// The index of the state the replay information should be returned for. - internal int[] GetReplayInformation(int stateIndex) - { - Requires.InRange(stateIndex, nameof(stateIndex), 0, _states.Length - 1); - return _replayInfo[stateIndex + 1]; - } - - /// - /// Replays the computation of the initial state. - /// - internal unsafe void ReplayInitialState() + /// The choice resolver that should be used to resolve nondeterministic choices. + /// The zero-based index of the transition that should be replayed. + internal unsafe void Replay(ChoiceResolver choiceResolver, int transitionIndex) { if (StepCount == 0) return; - var initialState = _states[0]; - fixed (byte* state = &initialState[0]) - RuntimeModel.Replay(state, _replayInfo[0], initializationStep: true); + choiceResolver.Clear(); + choiceResolver.PrepareNextState(); + choiceResolver.SetChoices(_replayInfo[transitionIndex]); + + fixed (byte* state = _states[transitionIndex]) + RuntimeModel.Deserialize(state); + + if (transitionIndex == 0) + RuntimeModel.ExecuteInitialStep(); + else + RuntimeModel.ExecuteStep(); + + RuntimeModel.NotifyFaultActivations(); } /// diff --git a/Source/SafetySharp/Analysis/ModelChecking/ActivationMinimalExecutedModel.cs b/Source/SafetySharp/Analysis/ModelChecking/ActivationMinimalExecutedModel.cs index 2688fcc6..371fa339 100644 --- a/Source/SafetySharp/Analysis/ModelChecking/ActivationMinimalExecutedModel.cs +++ b/Source/SafetySharp/Analysis/ModelChecking/ActivationMinimalExecutedModel.cs @@ -45,23 +45,25 @@ internal sealed class ActivationMinimalExecutedModel : ExecutedModel /// A factory function that creates the model instance that should be executed. /// The maximum number of successor states supported per state. internal ActivationMinimalExecutedModel(Func runtimeModelCreator, int successorStateCapacity) - : base(runtimeModelCreator) + : this(runtimeModelCreator, null, successorStateCapacity) { - var formulas = RuntimeModel.Formulas.Select(CompilationVisitor.Compile).ToArray(); - _transitions = new ActivationMinimalTransitionSetBuilder(RuntimeModel, successorStateCapacity, formulas); - _stateConstraints = CollectStateConstraints(); } /// /// Initializes a new instance. /// - /// The model instance that should be executed. + /// A factory function that creates the model instance that should be executed. + /// The formulas that should be evaluated for each state. /// The maximum number of successor states supported per state. - internal ActivationMinimalExecutedModel(RuntimeModel runtimeModel, int successorStateCapacity) - : base(runtimeModel) + internal ActivationMinimalExecutedModel(Func runtimeModelCreator, Func[] formulas, int successorStateCapacity) + : base(runtimeModelCreator) { - _transitions = new ActivationMinimalTransitionSetBuilder(RuntimeModel, successorStateCapacity); - _stateConstraints = CollectStateConstraints(); + formulas = formulas ?? RuntimeModel.Formulas.Select(CompilationVisitor.Compile).ToArray(); + + _transitions = new ActivationMinimalTransitionSetBuilder(RuntimeModel, successorStateCapacity, formulas); + _stateConstraints = RuntimeModel.Model.Components.Cast().SelectMany(component => component.StateConstraints).ToArray(); + + ChoiceResolver = new ChoiceResolver(RuntimeModel.Objects.OfType()); } /// @@ -69,14 +71,6 @@ internal ActivationMinimalExecutedModel(RuntimeModel runtimeModel, int successor /// public override unsafe int TransitionSize => sizeof(CandidateTransition); - /// - /// Collects all state constraints contained in the model. - /// - private Func[] CollectStateConstraints() - { - return RuntimeModel.Model.Components.Cast().SelectMany(component => component.StateConstraints).ToArray(); - } - /// /// Disposes the object, releasing all managed and unmanaged resources. /// diff --git a/Source/SafetySharp/Analysis/ModelChecking/ExecutedModel.cs b/Source/SafetySharp/Analysis/ModelChecking/ExecutedModel.cs index c1ad50fb..67419eed 100644 --- a/Source/SafetySharp/Analysis/ModelChecking/ExecutedModel.cs +++ b/Source/SafetySharp/Analysis/ModelChecking/ExecutedModel.cs @@ -67,6 +67,11 @@ internal ExecutedModel(RuntimeModel runtimeModel) /// public sealed override Func RuntimeModelCreator { get; } + /// + /// Gets or sets the choice resolver that is used to resolve choices within the model. + /// + protected ChoiceResolver ChoiceResolver { get; set; } + /// /// Gets the model's state vector layout. /// @@ -92,8 +97,11 @@ internal void ChangeFaultActivations(Func getActivation) /// If true, indicates that the object is disposed; otherwise, the object is finalized. protected override void OnDisposing(bool disposing) { - if (disposing) - RuntimeModel.SafeDispose(); + if (!disposing) + return; + + ChoiceResolver.SafeDispose(); + RuntimeModel.SafeDispose(); } /// @@ -129,11 +137,11 @@ protected override void OnDisposing(bool disposing) public override TransitionCollection GetInitialTransitions() { BeginExecution(); - RuntimeModel.ChoiceResolver.PrepareNextState(); + ChoiceResolver.PrepareNextState(); fixed (byte* state = RuntimeModel.ConstructionState) { - while (RuntimeModel.ChoiceResolver.PrepareNextPath()) + while (ChoiceResolver.PrepareNextPath()) { RuntimeModel.Deserialize(state); ExecuteInitialTransition(); @@ -152,9 +160,9 @@ public override TransitionCollection GetInitialTransitions() public override TransitionCollection GetSuccessorTransitions(byte* state) { BeginExecution(); - RuntimeModel.ChoiceResolver.PrepareNextState(); + ChoiceResolver.PrepareNextState(); - while (RuntimeModel.ChoiceResolver.PrepareNextPath()) + while (ChoiceResolver.PrepareNextPath()) { RuntimeModel.Deserialize(state); ExecuteTransition(); @@ -170,6 +178,7 @@ public override TransitionCollection GetSuccessorTransitions(byte* state) /// public sealed override void Reset() { + ChoiceResolver.Clear(); RuntimeModel.Reset(); } } diff --git a/Source/SafetySharp/Analysis/ModelChecking/StateGraph.cs b/Source/SafetySharp/Analysis/ModelChecking/StateGraph.cs index 8eff1708..b5a38cc7 100644 --- a/Source/SafetySharp/Analysis/ModelChecking/StateGraph.cs +++ b/Source/SafetySharp/Analysis/ModelChecking/StateGraph.cs @@ -125,7 +125,6 @@ internal sealed unsafe class StateGraph : DisposableObject internal void AddStateInfo(int state, bool isInitial, TransitionCollection transitions, int transitionCount) { Assert.That(!isInitial || _initialTransitionCount == 0, "Initial transitions can only be added once."); - Assert.That(transitionCount > 0, "Cannot add deadlock state."); if (isInitial) _initialTransitionCount = transitionCount; diff --git a/Source/SafetySharp/Analysis/Simulator.cs b/Source/SafetySharp/Analysis/Simulator.cs index 62c8260b..cc3edbaf 100644 --- a/Source/SafetySharp/Analysis/Simulator.cs +++ b/Source/SafetySharp/Analysis/Simulator.cs @@ -24,6 +24,7 @@ namespace SafetySharp.Analysis { using System; using System.Collections.Generic; + using System.Linq; using System.Runtime.InteropServices; using System.Text; using Modeling; @@ -33,26 +34,12 @@ namespace SafetySharp.Analysis /// /// Simulates a S# model for debugging or testing purposes. /// - public sealed unsafe class Simulator + public sealed unsafe class Simulator : DisposableObject { - /// - /// The counter example that is replayed by the simulator. - /// private readonly CounterExample _counterExample; - - /// - /// The runtime model that is simulated. - /// private readonly RuntimeModel _runtimeModel; - - /// - /// The states encountered by the simulator. - /// private readonly List _states = new List(); - - /// - /// The current state number of the simulator. - /// + private ChoiceResolver _choiceResolver; private int _stateIndex; /// @@ -188,6 +175,9 @@ public void Prune() /// public void Reset() { + if (_choiceResolver == null) + _choiceResolver = new ChoiceResolver(_runtimeModel.Objects.OfType()); + var state = stackalloc byte[_runtimeModel.StateVectorSize]; _states.Clear(); @@ -196,7 +186,7 @@ public void Reset() if (_counterExample == null) _runtimeModel.Reset(); else - _counterExample.ReplayInitialState(); + _counterExample.Replay(_choiceResolver, 0); _runtimeModel.Serialize(state); AddState(state); @@ -207,8 +197,7 @@ public void Reset() /// private void Replay() { - fixed (byte* sourceState = _states[_stateIndex - 1]) - _runtimeModel.Replay(sourceState, _counterExample.GetReplayInformation(_stateIndex - 1), initializationStep: _stateIndex == -1); + _counterExample.Replay(_choiceResolver, _stateIndex); var actualState = stackalloc byte[_runtimeModel.StateVectorSize]; _runtimeModel.Serialize(actualState); @@ -223,7 +212,7 @@ private void Replay() } /// - /// Ensures that the two states match. + /// Ensures that the two states match. /// private void EnsureStatesMatch(byte* actualState, byte[] expectedState) { @@ -260,5 +249,18 @@ private void RestoreState(int stateNumber) fixed (byte* state = _states[stateNumber]) _runtimeModel.Deserialize(state); } + + /// + /// Disposes the object, releasing all managed and unmanaged resources. + /// + /// If true, indicates that the object is disposed; otherwise, the object is finalized. + protected override void OnDisposing(bool disposing) + { + if (!disposing) + return; + + _counterExample.SafeDispose(); + _choiceResolver.SafeDispose(); + } } } \ No newline at end of file diff --git a/Source/SafetySharp/Runtime/ChoiceResolver.cs b/Source/SafetySharp/Runtime/ChoiceResolver.cs index 3a3f91e7..6fc561f2 100644 --- a/Source/SafetySharp/Runtime/ChoiceResolver.cs +++ b/Source/SafetySharp/Runtime/ChoiceResolver.cs @@ -23,10 +23,8 @@ namespace SafetySharp.Runtime { using System.Collections.Generic; - using System.Linq; using System.Runtime.CompilerServices; using Modeling; - using Serialization; using Utilities; /// @@ -63,11 +61,11 @@ internal sealed class ChoiceResolver : DisposableObject /// /// Initializes a new instance. /// - /// The object table containing all objects that potentially require access to the choice resolver. - public ChoiceResolver(ObjectTable objectTable) + /// The choices that potentially require access to the choice resolver. + public ChoiceResolver(IEnumerable choices) { - foreach (var obj in objectTable.OfType()) - obj.Resolver = this; + foreach (var choice in choices) + choice.Resolver = this; } /// diff --git a/Source/SafetySharp/Runtime/RuntimeModel.cs b/Source/SafetySharp/Runtime/RuntimeModel.cs index 6de79400..77d55086 100644 --- a/Source/SafetySharp/Runtime/RuntimeModel.cs +++ b/Source/SafetySharp/Runtime/RuntimeModel.cs @@ -115,7 +115,6 @@ internal RuntimeModel(SerializedRuntimeModel serializedData, int stateHeaderByte _stateHeaderBytes = stateHeaderBytes; PortBinding.BindAll(objectTable); - ChoiceResolver = new ChoiceResolver(objectTable); ConstructionState = new byte[StateVectorSize]; fixed (byte* state = ConstructionState) @@ -128,11 +127,6 @@ internal RuntimeModel(SerializedRuntimeModel serializedData, int stateHeaderByte StateFormulaSet.CheckFormulaCount(StateFormulas.Length); } - /// - /// Gets the used by the model. - /// - internal ChoiceResolver ChoiceResolver { get; } - /// /// Gets a copy of the original model the runtime model was generated from. /// @@ -251,8 +245,6 @@ internal void Reset() Deserialize(state); _restrictRanges(); } - - ChoiceResolver.Clear(); } /// @@ -294,7 +286,7 @@ internal void ExecuteStep() /// transitions could be generated for the model. /// /// Indicates whether the counter example ends with an exception. - public CounterExample CreateCounterExample(Func createModel, byte[][] path, bool endsWithException) + public CounterExample CreateCounterExample(Func createModel, byte[][] path,bool endsWithException) { Requires.NotNull(createModel, nameof(createModel)); @@ -302,6 +294,7 @@ public CounterExample CreateCounterExample(Func createModel, byte[ // state variables might prevent us from doing so if they somehow influence the state var replayModel = createModel(); var counterExampleModel = createModel(); + var choiceResolver = new ChoiceResolver(replayModel.Objects.OfType()); CopyFaultActivationStates(replayModel); CopyFaultActivationStates(counterExampleModel); @@ -312,22 +305,20 @@ public CounterExample CreateCounterExample(Func createModel, byte[ // we still have to get the choices that caused the problem. if (path == null) - { - path = new[] { ConstructionState, new byte[StateVectorSize] }; - return new CounterExample(counterExampleModel, path, new[] { GetLastChoices() }, endsWithException); - } + path = new[] { new byte[StateVectorSize] }; path = new[] { ConstructionState }.Concat(path).ToArray(); - var replayInfo = replayModel.GenerateReplayInformation(path, endsWithException); + var replayInfo = replayModel.GenerateReplayInformation(choiceResolver, path, endsWithException); return new CounterExample(counterExampleModel, path, replayInfo, endsWithException); } /// /// Generates the replay information for the . /// + /// The choice resolver that should be used to resolve nondeterministic choices. /// The trace the replay information should be generated for. /// Indicates whether the trace ends with an exception being thrown. - private int[][] GenerateReplayInformation(byte[][] trace, bool endsWithException) + private int[][] GenerateReplayInformation(ChoiceResolver choiceResolver, byte[][] trace, bool endsWithException) { var info = new int[trace.Length - 1][]; var targetState = stackalloc byte[StateVectorSize]; @@ -335,28 +326,34 @@ private int[][] GenerateReplayInformation(byte[][] trace, bool endsWithException // We have to generate the replay info for all transitions for (var i = 0; i < trace.Length - 1; ++i) { - ChoiceResolver.Clear(); - ChoiceResolver.PrepareNextState(); + choiceResolver.Clear(); + choiceResolver.PrepareNextState(); // Try all transitions until we find the one that leads to the desired state - while (ChoiceResolver.PrepareNextPath()) + while (true) { - fixed (byte* sourceState = trace[i]) - Deserialize(sourceState); - try { + if (!choiceResolver.PrepareNextPath()) + break; + + fixed (byte* sourceState = trace[i]) + Deserialize(sourceState); + if (i == 0) ExecuteInitialStep(); else ExecuteStep(); + + if (endsWithException && i == trace.Length - 2) + continue; } catch (Exception) { Requires.That(endsWithException, "Unexpected exception."); Requires.That(i == trace.Length - 2, "Unexpected exception."); - info[i] = ChoiceResolver.GetChoices().ToArray(); + info[i] = choiceResolver.GetChoices().ToArray(); break; } @@ -371,7 +368,7 @@ private int[][] GenerateReplayInformation(byte[][] trace, bool endsWithException if (!areEqual) continue; - info[i] = ChoiceResolver.GetChoices().ToArray(); + info[i] = choiceResolver.GetChoices().ToArray(); break; } @@ -381,31 +378,6 @@ private int[][] GenerateReplayInformation(byte[][] trace, bool endsWithException return info; } - /// - /// Replays the model step starting at the serialized using the given - /// . - /// - /// The serialized state that the replay starts from. - /// The replay information required to compute the target state. - /// Indicates whether the initialization step should be replayed. - internal void Replay(byte* state, int[] replayInformation, bool initializationStep) - { - Requires.NotNull(replayInformation, nameof(replayInformation)); - - ChoiceResolver.Clear(); - ChoiceResolver.PrepareNextState(); - ChoiceResolver.SetChoices(replayInformation); - - Deserialize(state); - - if (initializationStep) - ExecuteInitialStep(); - else - ExecuteStep(); - - NotifyFaultActivations(); - } - /// /// Notifies all activated faults of their activation. Returns false to indicate that no notifications were necessary. /// @@ -427,25 +399,14 @@ internal bool NotifyFaultActivations() return notificationsSent; } - /// - /// Gets the choices that were made to generate the last transitions. - /// - internal int[] GetLastChoices() - { - return ChoiceResolver.GetChoices().ToArray(); - } - /// /// Disposes the object, releasing all managed and unmanaged resources. /// /// If true, indicates that the object is disposed; otherwise, the object is finalized. protected override void OnDisposing(bool disposing) { - if (!disposing) - return; - - ChoiceResolver.SafeDispose(); - Objects.OfType().SafeDisposeAll(); + if (disposing) + Objects.OfType().SafeDisposeAll(); } ///