Skip to content

Commit

Permalink
Updated invariant computation plugin
Browse files Browse the repository at this point in the history
  • Loading branch information
Ruediger Ehlers committed Apr 3, 2024
1 parent ae09249 commit ab770fa
Show file tree
Hide file tree
Showing 7 changed files with 326 additions and 25 deletions.
2 changes: 1 addition & 1 deletion lib/subprocess.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -85,7 +85,7 @@ class popen
{
int status = 0;
pid_t ret = waitpid(pid, &status, 0);
if (ret==-1) {
if ((ret==-1) || (!(WIFEXITED(status)))) {
return -1; // Signal error.
}
return WEXITSTATUS(status);
Expand Down
3 changes: 2 additions & 1 deletion src/BFAbstractionLibrary/bddDump.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@
#include <fstream>
#include <algorithm>
#undef fail
#define MAX_NODES_GRAPH 100
#define MAX_NODES_GRAPH 300
using namespace std;

/**
Expand Down Expand Up @@ -241,6 +241,7 @@ void BF_newDumpDot(const VariableInfoContainer &cont, const BF &b, const char* v
else
dumpFile << "{ node [shape = box]; \"1\"; }}";
}
dumpFile << "\n";

// Print the Connections
for (unsigned int i=0;i<vars.size();i++) {
Expand Down
97 changes: 76 additions & 21 deletions src/extensionComputeInvariants.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -46,6 +46,7 @@ template<class T, bool supportForDontCare> class XComputeInvariants : public T {
using T::mgr;
using T::variables;
using T::variableNames;
using T::getVariableNumbersOfType;
using T::varVectorPre;
using T::varVectorPost;
using T::varCubePre;
Expand Down Expand Up @@ -125,7 +126,7 @@ template<class T, bool supportForDontCare> class XComputeInvariants : public T {
BF oldReachable = mgr.constantFalse();
while (reachable!=oldReachable) {
oldReachable = reachable;
reachable |= (safetyEnv & safetySys & reachable).ExistAbstract(varCubePre).SwapVariables(varVectorPre,varVectorPost);
reachable |= (safetyEnv & safetySys & reachable & winningPositions).ExistAbstract(varCubePre).SwapVariables(varVectorPre,varVectorPost);
//BF_newDumpDot(*this,reachable,NULL,"/tmp/currentreachable.dot");
}

Expand Down Expand Up @@ -266,6 +267,11 @@ template<class T, bool supportForDontCare> class XComputeInvariants : public T {
std::vector<int> startingVarsActiveBasesForEachNegativeExample;
int nofVarsSoFar = 0;


// Allocate SAT Solver
CaDiCaL::Solver solver;
unsigned int nofNegativeExamplesProcessedSoFar = 0;

// Allocate variables for invariant bases
for (int i=0;i<nofInvariants;i++) {
#ifndef NDEBUG \
Expand All @@ -275,9 +281,29 @@ template<class T, bool supportForDontCare> class XComputeInvariants : public T {
nofVarsSoFar += relevantCUDDVars.size();
}

// Allocate SAT Solver
CaDiCaL::Solver solver;
unsigned int nofNegativeExamplesProcessedSoFar = 0;
// Symmetry breaking: Invariant bases must be lexicographically ordered
for (int i=0;i<nofInvariants-1;i++) {
int startingVarDiff = nofVarsSoFar+1;
nofVarsSoFar += relevantCUDDVars.size();

// Start
solver.clause(startingVarsInvariantBases[i],startingVarsInvariantBases[i+1],-1*startingVarDiff);
solver.clause(-1*startingVarsInvariantBases[i],-1*startingVarsInvariantBases[i+1],-1*startingVarDiff);
// Continue
for (unsigned int j=0;j<relevantCUDDVars.size()-1;j++) {
solver.clause(startingVarDiff+j,startingVarsInvariantBases[i]+j+1,startingVarsInvariantBases[i+1]+j+1,-1*startingVarDiff-j-1);
solver.clause(startingVarDiff+j,-1*startingVarsInvariantBases[i]-j-1,-1*startingVarsInvariantBases[i+1]-j-1,-1*startingVarDiff-j-1);
}

// If no diff before, lexicographical
// Start
solver.clause(-1*startingVarsInvariantBases[i],startingVarsInvariantBases[i+1]);
// Continue
for (unsigned int j=0;j<relevantCUDDVars.size()-1;j++) {
solver.clause(startingVarDiff+j,-1*startingVarsInvariantBases[i]-j-1,startingVarsInvariantBases[i+1]+j+1);
}
}



while (true) {
Expand Down Expand Up @@ -458,7 +484,6 @@ template<class T, bool supportForDontCare> class XComputeInvariants : public T {
//std::istringstream is(stdoutBuffer.str());
//std::string currentline;

std::vector<bool> model(nofVarsSoFar+1);
/*while (std::getline(is,currentline)) {
//std::cerr << "Interpreting model line: " << currentline << std::endl;
if (currentline.substr(0,2)=="v ") {
Expand All @@ -473,9 +498,6 @@ template<class T, bool supportForDontCare> class XComputeInvariants : public T {
}
}
}*/
for (int i=1;i<=nofVarsSoFar;i++) {
model[i] = solver.val(i)>0;
}

#ifndef NDEBUG
//std::cerr << "Model read: ";
Expand All @@ -490,13 +512,13 @@ template<class T, bool supportForDontCare> class XComputeInvariants : public T {
}
for (unsigned int i=0;i<negativeExamples.size();i++) {
for (int j=0;j<nofInvariants;j++) {
if (model[startingVarsInvariantSelectorForNegativeExample[i]+j]) {
if (solver.val(startingVarsInvariantSelectorForNegativeExample[i]+j)>0) {
//std::cerr << "Negative example " << i << " is covered by invariant " << j << std::endl;

BF thisCase = mgr.constantTrue();
for (unsigned int k=0;k<relevantCUDDVars.size();k++) {
if (negativeExamples[i][k]!=0) {
if ((negativeExamples[i][k]>0) == (model[startingVarsInvariantBases[j]+k])) {
if ((negativeExamples[i][k]>0) == (solver.val(startingVarsInvariantBases[j]+k)>0)) {
if (negativeExamples[i][k]>0)
thisCase &= relevantCUDDVarBFs[k];
else if (negativeExamples[i][k]<0)
Expand All @@ -521,6 +543,7 @@ template<class T, bool supportForDontCare> class XComputeInvariants : public T {
}

BF rest = allInvariantsTogether & toBeCovered;
BF noNextBehavior = !((safetySys).ExistAbstract(varCubePostOutput));

if (rest.isFalse()) {

Expand All @@ -529,18 +552,20 @@ template<class T, bool supportForDontCare> class XComputeInvariants : public T {
for (int i=0;i<nofInvariants;i++) {
std::cout << "- Invariant " << i << " with base: ";
for (unsigned int k=0;k<relevantCUDDVars.size();k++) {
std::cout << ((model[startingVarsInvariantBases[i]+k]?"1":"0"));
std::cout << ((solver.val(startingVarsInvariantBases[i]+k)>0?"1":"0"));
}
std::cout << "\n";
for (unsigned int j=0;j<negativeExamples.size();j++) {
if (model[startingVarsInvariantSelectorForNegativeExample[j]+i]) {
if (solver.val(startingVarsInvariantSelectorForNegativeExample[j]+i)>0) {
std::cout << " - Example ";
for (auto it : negativeExamples[j]) {
if (it>0) std::cout << "1"; else { if (it<0) std::cout << "0"; else std::cout << "?"; }
}
std::cout << "\n";
}
}


}

// Generate and DOT-output optimizecd BDDs for the invariants
Expand All @@ -549,17 +574,47 @@ template<class T, bool supportForDontCare> class XComputeInvariants : public T {
std::ostringstream filename;
filename << "/tmp/invariant" << i << ".dot";

// Iterative simplification cycles
BF oldsimplified = mgr.constantFalse();
// Simplification
//BF oldsimplified = mgr.constantFalse();
BF simplified = invariants[i];
if (oldsimplified != simplified) {
oldsimplified = simplified;
simplified = simplified.optimizeRestrict(winningPositions | toBeCovered);
simplified = simplified.optimizeRestrict(reachable | toBeCovered);
//simplified = simplified.optimizeRestrict(reachable);
simplified = simplified.optimizeRestrict((winningPositions & reachable) | toBeCovered);
//if (oldsimplified != simplified) {
// oldsimplified = simplified;
simplified = simplified.optimizeRestrict(reachable);
//simplified = simplified.optimizeRestrict(reachable);
//simplified = simplified.optimizeRestrict((winningPositions & reachable) | toBeCovered);
//}
BF_newDumpDot(*this,simplified /*& variables[12] & variables[6] & variables[8]*/,NULL,filename.str());

std::ostringstream filename3;
filename3 << "/tmp/invariant" << i << "-unoptimized.dot";
BF_newDumpDot(*this,invariants[i],NULL,filename3.str());

// Also print the cases of immediate specifiction violation separately
std::ostringstream filename2;
filename2 << "/tmp/invariant" << i << "-rightaway.dot";
BF immediatelyViolated = !invariants[i] & reachable & noNextBehavior;
BF_newDumpDot(*this,immediatelyViolated,NULL,filename2.str());

// Globally Determinize case
if (!(immediatelyViolated.isFalse())) {
std::cout << "Reachable state immediately violating invariant " << i << " (using all variables declared in the input file in the order in which they are declared): ";
std::vector<unsigned int> varNums;
getVariableNumbersOfType("Pre", varNums);
for (auto it : varNums) {
if ((immediatelyViolated & variables[it]).isFalse()) {
std::cerr << "0";
immediatelyViolated &= !variables[it];
} else {
std::cerr << "1";
immediatelyViolated &= variables[it];
}
if (immediatelyViolated.isFalse()) throw "Internal error processing 'immediatelyViolated'";
}
std::cout << "\n";
}
BF_newDumpDot(*this,simplified,NULL,filename.str());



}

return;
Expand Down
3 changes: 2 additions & 1 deletion tools/StructuredSlugsParser/compiler.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -208,9 +208,10 @@ def parseLTL(ltlTxt,reasonForNotBeingASlugsFormula):
tree = p.parse(input)

except p.ParseErrors as exception:
print("Offending specification line: ",ltlTxt,file=sys.stderr)
for t,e in exception.errors:
if t[0] == p.EOF:
print >>sys.stderr, "Formula end not expected here"
print("Formula end not expected here",file=sys.stderr)
continue

found = repr(t[0])
Expand Down
2 changes: 1 addition & 1 deletion tools/cursesSimulator.py
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
#!/usr/bin/python
#!/usr/bin/env python2
#
# Interactive Strategy Simulator and Debugger for Slugs
import curses, sys, subprocess
Expand Down
68 changes: 68 additions & 0 deletions tools/dotBDDToBoolLabCommands.py
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,68 @@
#!/usr/bin/env python3
# This script takes a DOT output as generated by
# slugs and produces an equivalent Boolean expression
# for the Boollab, which you can find at:
#
# https://www.ruediger-ehlers.de/boollab/
#
# This allows you "play" with the boolean function
# and analyze it manually, for instance
# by reordering the variables manually until
# the Boolean function becomes easier to comprehend.
import os, sys

# Read input file
if len(sys.argv) < 2:
print("Error: No input file given.",file=sys.stderr)
sys.exit(1)
allLines = [a.strip() for a in open(sys.argv[1],"r").readlines()]

# Variables
vars = []
nodeToVar = {}
nodeListInOrder = []
for line in allLines:
if line.startswith("{ rank = same;"):
line = line[14:]
lineparts = [a.strip() for a in line.split(";")]
varName = lineparts[0][1:]
varName = varName[0:varName.find("-")]
if varName!="CONST NODES":
vars.append(varName)
for node in lineparts[1:]:
if len(node)>0:
node = node[1:len(node)-1]
nodeToVar[node] = varName
nodeListInOrder.append(node)

# Output vars
for var in vars:
print("var "+var)

# Nodes
nodesIn = {}
startFound = False
for line in allLines:
if line=="{ node [shape = box]; \"1\"; }}":
startFound = True
elif startFound:
if line.find("->")!=-1:
if line.find("[color=red];")!=-1:
negated = True
else:
negated = False
parts = line.split("\"")
fromNode = parts[1]
toNode = parts[3]
if not toNode in nodesIn:
nodesIn[toNode] = []
if negated:
nodesIn[toNode].append("(!"+nodeToVar[fromNode]+" & n"+fromNode+")")
else:
nodesIn[toNode].append("("+nodeToVar[fromNode]+" & n"+fromNode+")")

print("n"+nodeListInOrder[0]+" = 1")
for node in nodeListInOrder[1:] + ["1"]:
print("n"+node+" = "+"|".join(nodesIn[node]))

print("printBDD n1")
Loading

0 comments on commit ab770fa

Please sign in to comment.