Skip to content
Permalink
Browse files

Fixed Lustre_Model Tests 2

  • Loading branch information...
pascalpfeil committed Jun 5, 2018
1 parent b3e06c8 commit acbf6b5d0ff8a934cf0564b050829621fb038c82
@@ -51,7 +51,7 @@ public void CreateMarkovChainWithFalseFormula()
public void CreateMarkovChainWithHazards()
{
var markovChainGenerator = new MarkovChainFromExecutableModelGenerator<LustreExecutableModel>(_createModel) { Configuration = LustreModelChecker.TraversalConfiguration };
markovChainGenerator.Configuration.ModelCapacity = new ModelCapacityByModelSize(10000, 100000);
markovChainGenerator.Configuration.ModelCapacity = new ModelCapacityByModelSize(10000, 1000000);
markovChainGenerator.Configuration.SuccessorCapacity *= 2;
markovChainGenerator.AddFormulaToCheck(_hazard);
markovChainGenerator.Configuration.UseCompactStateStorage = true;
@@ -63,7 +63,7 @@ public void CreateMarkovChainWithHazards()
public void CreateMarkovChainWithHazardsWithoutStaticPruning()
{
var markovChainGenerator = new MarkovChainFromExecutableModelGenerator<LustreExecutableModel>(_createModel) { Configuration = LustreModelChecker.TraversalConfiguration };
markovChainGenerator.Configuration.ModelCapacity = new ModelCapacityByModelSize(10000, 100000);
markovChainGenerator.Configuration.ModelCapacity = new ModelCapacityByModelSize(10000, 1000000);
markovChainGenerator.Configuration.SuccessorCapacity *= 2;
markovChainGenerator.Configuration.EnableStaticPruningOptimization = false;
markovChainGenerator.AddFormulaToCheck(_hazard);
@@ -76,7 +76,7 @@ public void CreateMarkovChainWithHazardsWithoutStaticPruning()
public void CreateMarkovChainWithHazardRetraversal1()
{
var markovChainGenerator = new MarkovChainFromExecutableModelGenerator<LustreExecutableModel>(_createModel) { Configuration = LustreModelChecker.TraversalConfiguration };
markovChainGenerator.Configuration.ModelCapacity = new ModelCapacityByModelSize(10000, 100000);
markovChainGenerator.Configuration.ModelCapacity = new ModelCapacityByModelSize(10000, 1000000);
markovChainGenerator.Configuration.SuccessorCapacity *= 2;
markovChainGenerator.AddFormulaToCheck(_hazard);
markovChainGenerator.Configuration.UseCompactStateStorage = true;
@@ -95,7 +95,7 @@ public void CreateMarkovChainWithHazardRetraversal1()
public void CreateMarkovChainWithHazardsRetraversal2()
{
var markovChainGenerator = new MarkovChainFromExecutableModelGenerator<LustreExecutableModel>(_createModel) { Configuration = LustreModelChecker.TraversalConfiguration };
markovChainGenerator.Configuration.ModelCapacity = new ModelCapacityByModelSize(10000, 100000);
markovChainGenerator.Configuration.ModelCapacity = new ModelCapacityByModelSize(10000, 1000000);
markovChainGenerator.Configuration.SuccessorCapacity *= 2;
markovChainGenerator.AddFormulaToCheck(_hazard);
markovChainGenerator.Configuration.UseCompactStateStorage = true;
@@ -114,7 +114,7 @@ public void CreateMarkovChainWithHazardsRetraversal2()
public void CreateMarkovChainWithHazardFaultsInState()
{
var markovChainGenerator = new MarkovChainFromExecutableModelGenerator<LustreExecutableModel>(_createModel) { Configuration = LustreModelChecker.TraversalConfiguration };
markovChainGenerator.Configuration.ModelCapacity = new ModelCapacityByModelSize(10000, 100000);
markovChainGenerator.Configuration.ModelCapacity = new ModelCapacityByModelSize(10000, 1000000);
markovChainGenerator.Configuration.SuccessorCapacity *= 2;
markovChainGenerator.AddFormulaToCheck(_hazard);
foreach (var fault in _faults)
@@ -132,7 +132,7 @@ public void CreateMarkovChainWithHazardFaultsInState()
public void CreateFaultAwareMarkovChainAllFaults()
{
var markovChainGenerator = new MarkovChainFromExecutableModelGenerator<LustreExecutableModel>(_createModel) { Configuration = LustreModelChecker.TraversalConfiguration };
markovChainGenerator.Configuration.ModelCapacity = new ModelCapacityByModelSize(10000, 100000);
markovChainGenerator.Configuration.ModelCapacity = new ModelCapacityByModelSize(10000, 1000000);
markovChainGenerator.Configuration.SuccessorCapacity *= 2;
markovChainGenerator.Configuration.EnableStaticPruningOptimization = false;
markovChainGenerator.AddFormulaToCheck(_hazard);
@@ -262,7 +262,7 @@ public void CalculateLtmdpWithoutStaticPruningSingleCore()
var oldProbability = _faults[1].ProbabilityOfOccurrence;
_faults[1].ProbabilityOfOccurrence = null;
var markovChainGenerator = new MarkovDecisionProcessFromExecutableModelGenerator<LustreExecutableModel>(_createModel);
markovChainGenerator.Configuration.ModelCapacity = new ModelCapacityByModelSize(10000, 100000);
markovChainGenerator.Configuration.ModelCapacity = new ModelCapacityByModelSize(10000, 1000000);
markovChainGenerator.Configuration.SuccessorCapacity *= 2;
markovChainGenerator.Configuration.EnableStaticPruningOptimization = false;
markovChainGenerator.Configuration.LtmdpModelChecker = LtmdpModelChecker.BuiltInLtmdp;
@@ -292,7 +292,7 @@ public void CalculateMdpNewStates()
var oldProbability = _faults[1].ProbabilityOfOccurrence;
_faults[1].ProbabilityOfOccurrence = null;
var markovChainGenerator = new MarkovDecisionProcessFromExecutableModelGenerator<LustreExecutableModel>(_createModel);
markovChainGenerator.Configuration.ModelCapacity = new ModelCapacityByModelSize(10000, 100000);
markovChainGenerator.Configuration.ModelCapacity = new ModelCapacityByModelSize(10000, 1000000);
markovChainGenerator.Configuration.SuccessorCapacity *= 2;
markovChainGenerator.Configuration.EnableStaticPruningOptimization = false;
markovChainGenerator.Configuration.LtmdpModelChecker = LtmdpModelChecker.BuildInMdpWithNewStates;
@@ -316,7 +316,7 @@ public void CalculateMdpNewStatesConstant()
var oldProbability = _faults[1].ProbabilityOfOccurrence;
_faults[1].ProbabilityOfOccurrence = null;
var markovChainGenerator = new MarkovDecisionProcessFromExecutableModelGenerator<LustreExecutableModel>(_createModel);
markovChainGenerator.Configuration.ModelCapacity = new ModelCapacityByModelSize(10000, 100000);
markovChainGenerator.Configuration.ModelCapacity = new ModelCapacityByModelSize(10000, 1000000);
markovChainGenerator.Configuration.SuccessorCapacity *= 2;
markovChainGenerator.Configuration.EnableStaticPruningOptimization = false;
markovChainGenerator.Configuration.LtmdpModelChecker = LtmdpModelChecker.BuildInMdpWithNewStatesConstantDistance;
@@ -340,7 +340,7 @@ public void CalculateMdpFlattened()
var oldProbability = _faults[1].ProbabilityOfOccurrence;
_faults[1].ProbabilityOfOccurrence = null;
var markovChainGenerator = new MarkovDecisionProcessFromExecutableModelGenerator<LustreExecutableModel>(_createModel);
markovChainGenerator.Configuration.ModelCapacity = new ModelCapacityByModelSize(10000, 100000);
markovChainGenerator.Configuration.ModelCapacity = new ModelCapacityByModelSize(10000, 1000000);
markovChainGenerator.Configuration.SuccessorCapacity *= 2;
markovChainGenerator.Configuration.EnableStaticPruningOptimization = false;
markovChainGenerator.Configuration.LtmdpModelChecker = LtmdpModelChecker.BuildInMdpWithFlattening;
@@ -365,7 +365,7 @@ public void CalculateMdpNewStatesWithoutFaults()
var oldProbability = _faults[1].ProbabilityOfOccurrence;
_faults[1].ProbabilityOfOccurrence = null;
var markovChainGenerator = new MarkovDecisionProcessFromExecutableModelGenerator<LustreExecutableModel>(_createModel);
markovChainGenerator.Configuration.ModelCapacity = new ModelCapacityByModelSize(10000, 100000);
markovChainGenerator.Configuration.ModelCapacity = new ModelCapacityByModelSize(10000, 1000000);
markovChainGenerator.Configuration.SuccessorCapacity *= 2;
markovChainGenerator.Configuration.EnableStaticPruningOptimization = false;
markovChainGenerator.Configuration.LtmdpModelChecker = LtmdpModelChecker.BuildInMdpWithNewStates;
@@ -384,7 +384,7 @@ public void CalculateMdpNewStatesConstantWithoutFaults()
var oldProbability = _faults[1].ProbabilityOfOccurrence;
_faults[1].ProbabilityOfOccurrence = null;
var markovChainGenerator = new MarkovDecisionProcessFromExecutableModelGenerator<LustreExecutableModel>(_createModel);
markovChainGenerator.Configuration.ModelCapacity = new ModelCapacityByModelSize(10000, 100000);
markovChainGenerator.Configuration.ModelCapacity = new ModelCapacityByModelSize(10000, 1000000);
markovChainGenerator.Configuration.SuccessorCapacity *= 2;
markovChainGenerator.Configuration.EnableStaticPruningOptimization = false;
markovChainGenerator.Configuration.LtmdpModelChecker = LtmdpModelChecker.BuildInMdpWithNewStatesConstantDistance;
@@ -403,7 +403,7 @@ public void CalculateMdpFlattenedWithoutFaults()
var oldProbability = _faults[1].ProbabilityOfOccurrence;
_faults[1].ProbabilityOfOccurrence = null;
var markovChainGenerator = new MarkovDecisionProcessFromExecutableModelGenerator<LustreExecutableModel>(_createModel);
markovChainGenerator.Configuration.ModelCapacity = new ModelCapacityByModelSize(10000, 100000);
markovChainGenerator.Configuration.ModelCapacity = new ModelCapacityByModelSize(10000, 1000000);
markovChainGenerator.Configuration.SuccessorCapacity *= 2;
markovChainGenerator.Configuration.EnableStaticPruningOptimization = false;
markovChainGenerator.Configuration.LtmdpModelChecker = LtmdpModelChecker.BuildInMdpWithFlattening;
@@ -32,7 +32,7 @@ public void TankRupture()
var createModel = LustreExecutableModel.CreateExecutedModelFromFormulasCreator(Path.Combine(AssemblyDirectory, "pressureTank.lus"), "TANK", faults.ToArray());

var markovChainGenerator = new MarkovDecisionProcessFromExecutableModelGenerator<LustreExecutableModel>(createModel);
markovChainGenerator.Configuration.ModelCapacity = new ModelCapacityByModelSize(10000, 100000);
markovChainGenerator.Configuration.ModelCapacity = new ModelCapacityByModelSize(10000, 1000000);
markovChainGenerator.Configuration.SuccessorCapacity *= 2;
markovChainGenerator.Configuration.EnableStaticPruningOptimization = true;
markovChainGenerator.Configuration.LtmdpModelChecker = LtmdpModelChecker.BuiltInLtmdp;
@@ -40,39 +40,41 @@ namespace SafetyLustre.LustreCompiler
/// </summary>
public static class LusCompiler
{
private static readonly Object fileLock = new Object();
private static readonly Object mutex = new Object();

public static string Compile(string lustreSource, string mainNode)
{
SetupLus2Oc();
//HACK to make this thread safe
lock (mutex)
{
SetupLus2Oc();

var wslHomeDirectory = WslUtil.ExecuteCommandWithResult("echo $HOME") // Get home directory of current wsl user
.Trim(); // Remove trailing '\n'
var wslHomeDirectory = WslUtil.ExecuteCommandWithResult("echo $HOME") // Get home directory of current wsl user
.Trim(); // Remove trailing '\n'

var lxssHomeDirectory = Path.Combine(
Environment.GetEnvironmentVariable("localappdata"), // Wsl filesystem ist stored under
"lxss", // %localappdata%/lxss
wslHomeDirectory.Remove(0, 1) // Remove leading '/'
);
var lxssHomeDirectory = Path.Combine(
Environment.GetEnvironmentVariable("localappdata"), // Wsl filesystem is stored under
"lxss", // %localappdata%/lxss
wslHomeDirectory.Remove(0, 1) // Remove leading '/'
);

//HACK to make this thread safe
lock (fileLock)
{
// Store lustre source for lus2oc to read
File.WriteAllText(Path.Combine(lxssHomeDirectory, $"{mainNode}.lus"), lustreSource);
}

WslUtil.ExecuteCommand($"chmod 0777 {wslHomeDirectory}/{mainNode}.lus");
// Store lustre source for lus2oc to read
File.WriteAllText(Path.Combine(lxssHomeDirectory, $"{mainNode}.lus"), lustreSource);


// Compile .lus to wsl users home directory
WslUtil.ExecuteCommand(
$"export LUSTRE_INSTALL={wslHomeDirectory}/bin/lustre-v4-III-db-linux64;" + // Set environment variable
"source $LUSTRE_INSTALL/setenv.sh;" + // Source setenv script
$"lus2oc {wslHomeDirectory}/{mainNode}.lus {mainNode} -o {wslHomeDirectory}/{mainNode}.oc" // Compile .lus file
);
WslUtil.ExecuteCommand($"chmod 0777 {wslHomeDirectory}/{mainNode}.lus");

// Read and return compiled object code
return File.ReadAllText(Path.Combine(lxssHomeDirectory, $"{mainNode}.oc"));
// Compile .lus to wsl users home directory
WslUtil.ExecuteCommand(
$"export LUSTRE_INSTALL={wslHomeDirectory}/bin/lustre-v4-III-db-linux64;" + // Set environment variable
"source $LUSTRE_INSTALL/setenv.sh;" + // Source setenv script
$"lus2oc {wslHomeDirectory}/{mainNode}.lus {mainNode} -o {wslHomeDirectory}/{mainNode}.oc" // Compile .lus file
);

// Read and return compiled object code
return File.ReadAllText(Path.Combine(lxssHomeDirectory, $"{mainNode}.oc"));
}
}

/// <summary>
@@ -68,8 +68,13 @@ public virtual void SetInitialState()

public void Update()
{
var value = Choice.Choose(true, false);
Runner.Tick(value);
var inputs = new List<object>();
for (int i = 0; i < Runner.Oc5ModelState.InputMappings.Count; i++)
{
inputs.Add(Choice.Choose(true, false));
}

Runner.Tick(inputs.ToArray());

Outputs = Runner.Oc5ModelState.GetOutputs().ToList();
}

0 comments on commit acbf6b5

Please sign in to comment.
You can’t perform that action at this time.