Skip to content

Commit

Permalink
cleaned up LtsMin integration; moved ChoiceResolver handling out of R…
Browse files Browse the repository at this point in the history 
…untimeModel
  • Loading branch information
@axel-habermaier
axel-habermaier committed Jul 11, 2016
1 parent 70a2499 commit 18a5e44
Show file tree
Hide file tree
Showing 8 changed files with 98 additions and 131 deletions.
12 changes: 7 additions & 5 deletions Source/LtsMin/LtsMin.cpp
View file
Expand Up @@ -97,6 +97,7 @@ ref struct Globals
{
static ActivationMinimalExecutedModel^ ExecutedModel;
static RuntimeModel^ RuntimeModel;
static const char* ModelFile;
};

//---------------------------------------------------------------------------------------------------------------------------
Expand All @@ -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<RuntimeModel^>(&CreateModel), gcnew array<Func<bool>^>(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;
Expand Down
32 changes: 17 additions & 15 deletions Source/SafetySharp/Analysis/CounterExample.cs
View file
Expand Up @@ -119,26 +119,28 @@ public unsafe ModelBase DeserializeState(int position)
}

/// <summary>
/// Gets the replay information for the state identified by the zero-based <paramref name="stateIndex" />.
/// Replays the transition of the counter example with the zero-baesd <paramref name="transitionIndex" />.
/// </summary>
/// <param name="stateIndex">The index of the state the replay information should be returned for.</param>
internal int[] GetReplayInformation(int stateIndex)
{
Requires.InRange(stateIndex, nameof(stateIndex), 0, _states.Length - 1);
return _replayInfo[stateIndex + 1];
}

/// <summary>
/// Replays the computation of the initial state.
/// </summary>
internal unsafe void ReplayInitialState()
/// <param name="choiceResolver">The choice resolver that should be used to resolve nondeterministic choices.</param>
/// <param name="transitionIndex">The zero-based index of the transition that should be replayed.</param>
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();
}

/// <summary>
Expand Down
28 changes: 11 additions & 17 deletions Source/SafetySharp/Analysis/ModelChecking/ActivationMinimalExecutedModel.cs
View file
Expand Up @@ -45,38 +45,32 @@ internal sealed class ActivationMinimalExecutedModel : ExecutedModel
/// <param name="runtimeModelCreator">A factory function that creates the model instance that should be executed.</param>
/// <param name="successorStateCapacity">The maximum number of successor states supported per state.</param>
internal ActivationMinimalExecutedModel(Func<RuntimeModel> 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();
}

/// <summary>
/// Initializes a new instance.
/// </summary>
/// <param name="runtimeModel">The model instance that should be executed.</param>
/// <param name="runtimeModelCreator">A factory function that creates the model instance that should be executed.</param>
/// <param name="formulas">The formulas that should be evaluated for each state.</param>
/// <param name="successorStateCapacity">The maximum number of successor states supported per state.</param>
internal ActivationMinimalExecutedModel(RuntimeModel runtimeModel, int successorStateCapacity)
: base(runtimeModel)
internal ActivationMinimalExecutedModel(Func<RuntimeModel> runtimeModelCreator, Func<bool>[] 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<Component>().SelectMany(component => component.StateConstraints).ToArray();

ChoiceResolver = new ChoiceResolver(RuntimeModel.Objects.OfType<Choice>());
}

/// <summary>
/// Gets the size of a single transition of the model in bytes.
/// </summary>
public override unsafe int TransitionSize => sizeof(CandidateTransition);

/// <summary>
/// Collects all state constraints contained in the model.
/// </summary>
private Func<bool>[] CollectStateConstraints()
{
return RuntimeModel.Model.Components.Cast<Component>().SelectMany(component => component.StateConstraints).ToArray();
}

/// <summary>
/// Disposes the object, releasing all managed and unmanaged resources.
/// </summary>
Expand Down
21 changes: 15 additions & 6 deletions Source/SafetySharp/Analysis/ModelChecking/ExecutedModel.cs
View file
Expand Up @@ -67,6 +67,11 @@ internal ExecutedModel(RuntimeModel runtimeModel)
/// </summary>
public sealed override Func<RuntimeModel> RuntimeModelCreator { get; }

/// <summary>
/// Gets or sets the choice resolver that is used to resolve choices within the model.
/// </summary>
protected ChoiceResolver ChoiceResolver { get; set; }

/// <summary>
/// Gets the model's state vector layout.
/// </summary>
Expand All @@ -92,8 +97,11 @@ internal void ChangeFaultActivations(Func<Fault, Activation> getActivation)
/// <param name="disposing">If true, indicates that the object is disposed; otherwise, the object is finalized.</param>
protected override void OnDisposing(bool disposing)
{
if (disposing)
RuntimeModel.SafeDispose();
if (!disposing)
return;

ChoiceResolver.SafeDispose();
RuntimeModel.SafeDispose();
}

/// <summary>
Expand Down Expand Up @@ -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();
Expand All @@ -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();
Expand All @@ -170,6 +178,7 @@ public override TransitionCollection GetSuccessorTransitions(byte* state)
/// </summary>
public sealed override void Reset()
{
ChoiceResolver.Clear();
RuntimeModel.Reset();
}
}
Expand Down
1 change: 0 additions & 1 deletion Source/SafetySharp/Analysis/ModelChecking/StateGraph.cs
View file
Expand Up @@ -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;
Expand Down
42 changes: 22 additions & 20 deletions Source/SafetySharp/Analysis/Simulator.cs
View file
Expand Up @@ -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;
Expand All @@ -33,26 +34,12 @@ namespace SafetySharp.Analysis
/// <summary>
/// Simulates a S# model for debugging or testing purposes.
/// </summary>
public sealed unsafe class Simulator
public sealed unsafe class Simulator : DisposableObject
{
/// <summary>
/// The counter example that is replayed by the simulator.
/// </summary>
private readonly CounterExample _counterExample;

/// <summary>
/// The runtime model that is simulated.
/// </summary>
private readonly RuntimeModel _runtimeModel;

/// <summary>
/// The states encountered by the simulator.
/// </summary>
private readonly List<byte[]> _states = new List<byte[]>();

/// <summary>
/// The current state number of the simulator.
/// </summary>
private ChoiceResolver _choiceResolver;
private int _stateIndex;

/// <summary>
Expand Down Expand Up @@ -188,6 +175,9 @@ public void Prune()
/// </summary>
public void Reset()
{
if (_choiceResolver == null)
_choiceResolver = new ChoiceResolver(_runtimeModel.Objects.OfType<Choice>());

var state = stackalloc byte[_runtimeModel.StateVectorSize];

_states.Clear();
Expand All @@ -196,7 +186,7 @@ public void Reset()
if (_counterExample == null)
_runtimeModel.Reset();
else
_counterExample.ReplayInitialState();
_counterExample.Replay(_choiceResolver, 0);

_runtimeModel.Serialize(state);
AddState(state);
Expand All @@ -207,8 +197,7 @@ public void Reset()
/// </summary>
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);
Expand All @@ -223,7 +212,7 @@ private void Replay()
}

/// <summary>
/// Ensures that the two states match.
/// Ensures that the two states match.
/// </summary>
private void EnsureStatesMatch(byte* actualState, byte[] expectedState)
{
Expand Down Expand Up @@ -260,5 +249,18 @@ private void RestoreState(int stateNumber)
fixed (byte* state = _states[stateNumber])
_runtimeModel.Deserialize(state);
}

/// <summary>
/// Disposes the object, releasing all managed and unmanaged resources.
/// </summary>
/// <param name="disposing">If true, indicates that the object is disposed; otherwise, the object is finalized.</param>
protected override void OnDisposing(bool disposing)
{
if (!disposing)
return;

_counterExample.SafeDispose();
_choiceResolver.SafeDispose();
}
}
}
10 changes: 4 additions & 6 deletions Source/SafetySharp/Runtime/ChoiceResolver.cs
View file
Expand Up @@ -23,10 +23,8 @@
namespace SafetySharp.Runtime
{
using System.Collections.Generic;
using System.Linq;
using System.Runtime.CompilerServices;
using Modeling;
using Serialization;
using Utilities;

/// <summary>
Expand Down Expand Up @@ -63,11 +61,11 @@ internal sealed class ChoiceResolver : DisposableObject
/// <summary>
/// Initializes a new instance.
/// </summary>
/// <param name="objectTable">The object table containing all objects that potentially require access to the choice resolver.</param>
public ChoiceResolver(ObjectTable objectTable)
/// <param name="choices">The choices that potentially require access to the choice resolver.</param>
public ChoiceResolver(IEnumerable<Choice> choices)
{
foreach (var obj in objectTable.OfType<Choice>())
obj.Resolver = this;
foreach (var choice in choices)
choice.Resolver = this;
}

/// <summary>
Expand Down

0 comments on commit 18a5e44

Please sign in to comment.