diff --git a/lib/subprocess.hpp b/lib/subprocess.hpp index 270b691..03f7c8c 100644 --- a/lib/subprocess.hpp +++ b/lib/subprocess.hpp @@ -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); diff --git a/src/BFAbstractionLibrary/bddDump.cpp b/src/BFAbstractionLibrary/bddDump.cpp index 7343fc2..455abaf 100755 --- a/src/BFAbstractionLibrary/bddDump.cpp +++ b/src/BFAbstractionLibrary/bddDump.cpp @@ -13,7 +13,7 @@ #include #include #undef fail -#define MAX_NODES_GRAPH 100 +#define MAX_NODES_GRAPH 300 using namespace std; /** @@ -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 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; @@ -125,7 +126,7 @@ template 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"); } @@ -266,6 +267,11 @@ template class XComputeInvariants : public T { std::vector startingVarsActiveBasesForEachNegativeExample; int nofVarsSoFar = 0; + + // Allocate SAT Solver + CaDiCaL::Solver solver; + unsigned int nofNegativeExamplesProcessedSoFar = 0; + // Allocate variables for invariant bases for (int i=0;i 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 class XComputeInvariants : public T { //std::istringstream is(stdoutBuffer.str()); //std::string currentline; - std::vector model(nofVarsSoFar+1); /*while (std::getline(is,currentline)) { //std::cerr << "Interpreting model line: " << currentline << std::endl; if (currentline.substr(0,2)=="v ") { @@ -473,9 +498,6 @@ template class XComputeInvariants : public T { } } }*/ - for (int i=1;i<=nofVarsSoFar;i++) { - model[i] = solver.val(i)>0; - } #ifndef NDEBUG //std::cerr << "Model read: "; @@ -490,13 +512,13 @@ template class XComputeInvariants : public T { } for (unsigned int i=0;i0) { //std::cerr << "Negative example " << i << " is covered by invariant " << j << std::endl; BF thisCase = mgr.constantTrue(); for (unsigned int k=0;k0) == (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) @@ -521,6 +543,7 @@ template class XComputeInvariants : public T { } BF rest = allInvariantsTogether & toBeCovered; + BF noNextBehavior = !((safetySys).ExistAbstract(varCubePostOutput)); if (rest.isFalse()) { @@ -529,11 +552,11 @@ template class XComputeInvariants : public T { for (int i=0;i0?"1":"0")); } std::cout << "\n"; for (unsigned int j=0;j0) { std::cout << " - Example "; for (auto it : negativeExamples[j]) { if (it>0) std::cout << "1"; else { if (it<0) std::cout << "0"; else std::cout << "?"; } @@ -541,6 +564,8 @@ template class XComputeInvariants : public T { std::cout << "\n"; } } + + } // Generate and DOT-output optimizecd BDDs for the invariants @@ -549,17 +574,47 @@ template 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 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; diff --git a/tools/StructuredSlugsParser/compiler.py b/tools/StructuredSlugsParser/compiler.py index e09ee52..822bf54 100755 --- a/tools/StructuredSlugsParser/compiler.py +++ b/tools/StructuredSlugsParser/compiler.py @@ -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]) diff --git a/tools/cursesSimulator.py b/tools/cursesSimulator.py index c9b2034..effeff2 100755 --- a/tools/cursesSimulator.py +++ b/tools/cursesSimulator.py @@ -1,4 +1,4 @@ -#!/usr/bin/python +#!/usr/bin/env python2 # # Interactive Strategy Simulator and Debugger for Slugs import curses, sys, subprocess diff --git a/tools/dotBDDToBoolLabCommands.py b/tools/dotBDDToBoolLabCommands.py new file mode 100755 index 0000000..32993f4 --- /dev/null +++ b/tools/dotBDDToBoolLabCommands.py @@ -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") \ No newline at end of file diff --git a/tools/findMinimalSysTransSubsetMakingAGivenInitialStateLosingAfterAtMostOneStep.py b/tools/findMinimalSysTransSubsetMakingAGivenInitialStateLosingAfterAtMostOneStep.py new file mode 100755 index 0000000..b651239 --- /dev/null +++ b/tools/findMinimalSysTransSubsetMakingAGivenInitialStateLosingAfterAtMostOneStep.py @@ -0,0 +1,176 @@ +#!/usr/bin/env python3 +# A script for checking for a given initial state +# which sys_trans constraints are responsible for making it losing after at most one step. +import os, sys, tempfile, subprocess, time + +def checkRealizability(basepath,parameter): + ''' + This functions calls a script and looks out for lines stating realizability/unrealizability by Slugs. + It returns an error message if the subprocess returned with a non-zero errorcode or if multiple results are found. + Otherwise, the result is True or False. + ''' + slugsProcess = subprocess.Popen(basepath+"../src/slugs "+str(parameter), shell=True, bufsize=1048000, stdout=subprocess.PIPE,stderr=subprocess.STDOUT) + + nofRealizableLines = 0 + nofUnrealizableLines = 0 + lastLines = [] + + for line in slugsProcess.stdout.readlines(): + line = line.strip().decode("utf-8") + print("O: ",line) + if len(lastLines)>100: + lastLines = lastLines[1:]+[line] + else: + lastLines.append(line) + if line=="RESULT: Specification is realizable.": + nofRealizableLines +=1 + elif line=="RESULT: Specification is unrealizable.": + nofUnrealizableLines +=1 + + errorCode = slugsProcess.wait() + if (errorCode!=0): + errorMessage = "External tool or script terminated with a non-zero error code: "+str(errorCode)+"\n"+"\n".join(lastLines) + return errorMessage + if (nofRealizableLines+nofUnrealizableLines)>1: + return "Found more than one realizability/unrealizability result!" + if (nofRealizableLines+nofUnrealizableLines)==0: + return "Found no realizability/unrealizability result!" + if nofRealizableLines>0: + return True + elif nofUnrealizableLines>0: + return False + else: + raise Exception("Internal error. Should not be able to happen.") + + + +# Read parameters +if len(sys.argv)<3: + print("Error: Need input file (structuredslugs) and initial state",file=sys.stderr) + sys.exit(1) + +inputFile = sys.argv[1] +initialState = sys.argv[2] +basepath = os.path.realpath(__file__) +basepath = basepath[0:basepath.rfind("/")] + "/" + + +# READ INPUT FILE +segments = {"ENV_TRANS":[],"SYS_TRANS":[],"ENV_LIVENESS":[],"SYS_LIVENESS":[],"ENV_INIT":[],"SYS_INIT":[],"INPUT":[],"OUTPUT":[]} +currentSegment = "" +for line in open(inputFile,"r").readlines(): + line = line.strip() + if line.startswith("#") or len(line)==0: + pass + elif line.startswith("["): + currentSegment = line[1:len(line)-1] + else: + segments[currentSegment].append(line) + +# Perform analysis +with tempfile.TemporaryDirectory() as tmpDir: + + # First, get list of decoded variables + assert os.system(basepath+"../tools/StructuredSlugsParser/compiler.py "+inputFile+" > "+tmpDir+"/initial.slugsin")==0 + + inputAndOutputVarsEncoded = [] + currentSegment = False + currentOutput = False + for line in open(tmpDir+"/initial.slugsin","r").readlines(): + line = line.strip() + if line.startswith("#") or len(line)==0: + pass + elif line == "[INPUT]" or line=="[OUTPUT]": + currentSegment = True + if line=="[OUTPUT]": + currentOutput = True + elif line.startswith("["): + currentSegment = False + else: + if currentSegment: + inputAndOutputVarsEncoded.append((line,currentOutput)) + + # Now translate.... + currentPointerSysTrans = 0 + firstRound = True + while currentPointerSysTranscurrentPointerSysTrans: + outFile.write("AFTERFIRSTSTEP | ("+a+")\n") + + # Now try to translate + assert os.system(basepath+"../tools/StructuredSlugsParser/compiler.py "+tmpDir+"/try.structuredslugs > "+tmpDir+"/try.slugsin")==0 + + # Add initial state information + with open(tmpDir+"/try.slugsin","a") as outFile: + outFile.write("\n") + if firstRound: + print("Initial State:") + for i,(varname,vartype) in enumerate(inputAndOutputVarsEncoded): + if vartype: + outFile.write("[SYS_INIT]\n") + else: + outFile.write("[ENV_INIT]\n") + if initialState[i]=="0": + outFile.write("! "+varname+"\n") + if firstRound: + print("! "+varname) + elif initialState[i]=="1": + outFile.write(varname+"\n") + if firstRound: + print(varname) + else: + print("Error: Initial state contains character other than 0 and 1!",file=sys.stderr) + sys.exit(1) + + if len(initialState)>len(inputAndOutputVarsEncoded): + print("Error: Initial state string is too long.",file=sys.stderr) + sys.exit(1) + + firstRound = False + + realizable = checkRealizability(basepath,tmpDir+"/try.slugsin") + + if realizable is False: + segments["SYS_TRANS"] = segments["SYS_TRANS"][0:currentPointerSysTrans]+segments["SYS_TRANS"][currentPointerSysTrans+1:] + elif realizable is True: + currentPointerSysTrans += 1 + else: + print("Slugs call failed: ",realizable) + sys.exit(1) + + + print("Done") + # time.sleep(5000000) + +print("================Specification parts needed for this case: ====================") +for a in segments["SYS_TRANS"]: + print(a)