Skip to content

Commit

Permalink
Removed old "SATSolver.py" mentioning (not used any more), updated co…
Browse files Browse the repository at this point in the history 
…mmand line option for the "computeInvariants" plugin
  • Loading branch information
Ruediger Ehlers committed May 3, 2024
1 parent a0c2893 commit 13218b5
Show file tree
Hide file tree
Showing 5 changed files with 31 additions and 45 deletions.
4 changes: 2 additions & 2 deletions examples/genbuffer_from_anzu/run_all.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -22,8 +22,8 @@

foundInvariantNumber = True
# --computeInvariantsDontCare
print("Execute: ","../../src/slugs --computeInvariants "+base+".slugsin ../../src/satSolver.py "+str(currentInvariantNumber)+" > "+base+".invariant 2>&1")
assert os.system("../../src/slugs --computeInvariants "+base+".slugsin ../../src/satSolver.py "+str(currentInvariantNumber)+" " + " ".join(negativeExamplesCarriedOver) + " > "+base+".invariant 2>&1")==0
print("Execute: ","../../src/slugs --computeInvariants "+base+".slugsin "+str(currentInvariantNumber)+" > "+base+".invariant 2>&1")
assert os.system("../../src/slugs --computeInvariants "+base+".slugsin "+str(currentInvariantNumber)+" " + " ".join(negativeExamplesCarriedOver) + " > "+base+".invariant 2>&1")==0
with open(base+".invariant","r") as inFile:
allLines = inFile.readlines()
for line in allLines:
Expand Down
4 changes: 2 additions & 2 deletions examples/guiStepByStep/run_all.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -22,8 +22,8 @@

foundInvariantNumber = True
# --computeInvariantsDontCare
print("Execute: ","../../src/slugs --computeInvariants "+base+".slugsin ../../src/satSolver.py "+str(currentInvariantNumber)+" > "+base+".invariant 2>&1")
os.system("../../src/slugs --computeInvariants "+base+".slugsin ../../src/satSolver.py "+str(currentInvariantNumber)+" " + " ".join(negativeExamplesCarriedOver) + " > "+base+".invariant 2>&1")==0
print("Execute: ","../../src/slugs --computeInvariants "+base+".slugsin "+str(currentInvariantNumber)+" > "+base+".invariant 2>&1")
os.system("../../src/slugs --computeInvariants "+base+".slugsin "+str(currentInvariantNumber)+" " + " ".join(negativeExamplesCarriedOver) + " > "+base+".invariant 2>&1")==0
with open(base+".invariant","r") as inFile:
allLines = inFile.readlines()
for line in allLines:
Expand Down
52 changes: 19 additions & 33 deletions src/extensionComputeInvariants.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -32,7 +32,7 @@ class hashDdNodeUIntPair {
/**
* A class for computing invariants implied by the maximally permissive strategy (and probably later a bit more)
*/
template<class T, bool supportForDontCare> class XComputeInvariants : public T {
template<class T, bool beMoreStrict> class XComputeInvariants : public T {
protected:

using T::initSys;
Expand All @@ -59,24 +59,19 @@ template<class T, bool supportForDontCare> class XComputeInvariants : public T {
using T::computeWinningPositions;
using T::winningPositions;

std::string satSolver;
int nofInvariants;
std::vector<std::vector<int> > negativeExamples; // +1: TRUE, -1: FALSE, 0: don't care

XComputeInvariants<T,supportForDontCare>(std::list<std::string> &filenames) : T(filenames) {
XComputeInvariants<T,beMoreStrict>(std::list<std::string> &filenames) : T(filenames) {
}

void init(std::list<std::string> &filenames) {
T::init(filenames);

if (filenames.size()<2) {
throw SlugsException(false,"Error: Need file name of SAT solver and number of invariants to analyze invariants.");
if (filenames.size()<1) {
throw SlugsException(false,"Error: Need number of invariants to analyze invariants.");
}

satSolver = filenames.front();
filenames.pop_front();
std::cerr << "Using SAT Solver: " << satSolver << std::endl;

std::istringstream is(filenames.front());
filenames.pop_front();
is >> nofInvariants;
Expand Down Expand Up @@ -133,8 +128,6 @@ template<class T, bool supportForDontCare> class XComputeInvariants : public T {
//BF_newDumpDot(*this,reachable,NULL,"/tmp/currentreachable.dot");
}*/

const bool beMoreStrict = false;

// Compute states that are reachable when assumptions and guarantees are always satisfied.
// ...both by going only through winning positions and not
BF reachableAndWinning = beMoreStrict?(initEnv & initSys):(initEnv & initSys & winningPositions); //& winningPositions;
Expand Down Expand Up @@ -888,30 +881,23 @@ template<class T, bool supportForDontCare> class XComputeInvariants : public T {
std::vector<int> nextNegativeExample;
for (unsigned int k=0;k<relevantCUDDVars.size();k++) {
// Which direction to prefer is random to make negative examples for uniform
if (supportForDontCare && ((rest & relevantCUDDVarBFs[k]).ExistAbstractSingleVar(relevantCUDDVarBFs[k]) == (rest & !relevantCUDDVarBFs[k]).ExistAbstractSingleVar(relevantCUDDVarBFs[k]))) {
// Dont't case!
nextNegativeExample.push_back(0);
} else {
if (rng() & 1) {
if ((rest & relevantCUDDVarBFs[k]).isFalse()) {
nextNegativeExample.push_back(-1);
rest &= !relevantCUDDVarBFs[k];
} else {
nextNegativeExample.push_back(1);
rest &= relevantCUDDVarBFs[k];
}
if (rng() & 1) {
if ((rest & relevantCUDDVarBFs[k]).isFalse()) {
nextNegativeExample.push_back(-1);
rest &= !relevantCUDDVarBFs[k];
} else {
if ((rest & !relevantCUDDVarBFs[k]).isFalse()) {
nextNegativeExample.push_back(1);
rest &= relevantCUDDVarBFs[k];
} else {
nextNegativeExample.push_back(-1);
rest &= !relevantCUDDVarBFs[k];
}
nextNegativeExample.push_back(1);
rest &= relevantCUDDVarBFs[k];
}
} else {
if ((rest & !relevantCUDDVarBFs[k]).isFalse()) {
nextNegativeExample.push_back(1);
rest &= relevantCUDDVarBFs[k];
} else {
nextNegativeExample.push_back(-1);
rest &= !relevantCUDDVarBFs[k];
}
}

// TODO: Can this be done in a smarter way? Enumerating some cube instead?
}

std::cerr << "New negative example (no." << negativeExamples.size() << "): ";
Expand Down Expand Up @@ -952,7 +938,7 @@ template<class T, bool supportForDontCare> class XComputeInvariants : public T {

public:
static GR1Context* makeInstance(std::list<std::string> &filenames) {
return new XComputeInvariants<T,supportForDontCare>(filenames);
return new XComputeInvariants<T,beMoreStrict>(filenames);
}
};

Expand Down
4 changes: 2 additions & 2 deletions src/main.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -99,7 +99,7 @@ const char *commandLineArguments[] = {
"--environmentFriendlySynthesis","Performs environment-friendly realizability checking according to the construction from the TACAS 2019 paper 'Environmentally-friendly GR(1) Synthesis' by Majumdar, Piterman, and Schmuck, using a quadruply nested fixpoint.",
"--useHeuristic","Modifier for --environmentFriendlySynthesis: When computing winningPositions for environment-friendly strategies a sound but incomplete heuristic is used which only explores b==a within EnvironmentFriendlySynthesis.",
"--computeInvariants","Compute invariants that explain a synthesized strategy and/or the strategic choices that need to be made by an implementation of the specification",
"--computeInvariantsDontCare","Add don't care support for the '--computeInvariants' plugin, which can simplify the invariants but makes distributing the counter-examples to invariants less precise.",
"--computeInvariantsBeMoreStrict","Increase the initially reachable states in the '--computeInvariants' plugin beyond the initial winning ones, and consider invariants capturing all non-winning states. This makes some computed invariants easier to read.",
//-END-COMMAND-LINE-ARGUMENT-LIST
};

Expand Down Expand Up @@ -173,7 +173,7 @@ OptionCombination optionCombinations[] = {
OptionCombination("--computeCNFFormOfTheSpecification",XComputeCNFFormOfTheSpecification<GR1Context>::makeInstance),
OptionCombination("--computeIncompleteInformationEstimator",XIncompleteInformationEstimatorSynthesis<GR1Context>::makeInstance),
OptionCombination("--computeInterestingRunOfTheSystem",XComputeInterestingRunOfTheSystem<GR1Context>::makeInstance),
OptionCombination("--computeInvariants --computeInvariantsDontCare",XComputeInvariants<GR1Context,true>::makeInstance),
OptionCombination("--computeInvariants --computeInvariantsBeMoreStrict",XComputeInvariants<GR1Context,true>::makeInstance),
OptionCombination("--computeInvariants",XComputeInvariants<GR1Context,false>::makeInstance),
OptionCombination("--computeWeakenedSafetyAssumptions",XComputeWeakenedSafetyAssumptions<GR1Context>::makeInstance),
OptionCombination("--cooperativeGR1Strategy --explicitStrategy --jsonOutput --simpleRecovery --sysInitRoboticsSemantics",XExtractExplicitStrategy<XRoboticsSemantics<XCooperativeGR1Strategy<GR1Context>>,true,true>::makeInstance),
Expand Down
12 changes: 6 additions & 6 deletions src/plugin_combination_enumerator.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -77,7 +77,7 @@ def simpleInstantiationMapper(param,templateName,params):
("environmentFriendlySynthesis","Performs environment-friendly realizability checking according to the construction from the TACAS 2019 paper 'Environmentally-friendly GR(1) Synthesis' by Majumdar, Piterman, and Schmuck, using a quadruply nested fixpoint."),
("useHeuristic","Modifier for --environmentFriendlySynthesis: When computing winningPositions for environment-friendly strategies a sound but incomplete heuristic is used which only explores b==a within EnvironmentFriendlySynthesis."),
("computeInvariants","Compute invariants that explain a synthesized strategy and/or the strategic choices that need to be made by an implementation of the specification"),
("computeInvariantsDontCare","Add don't care support for the '--computeInvariants' plugin, which can simplify the invariants but makes distributing the counter-examples to invariants less precise.")
("computeInvariantsBeMoreStrict","Increase the initially reachable states in the '--computeInvariants' plugin beyond the initial winning ones, and consider invariants capturing all non-winning states. This makes some computed invariants easier to read.")
]

# Which command line parameters can be combined?
Expand Down Expand Up @@ -171,7 +171,7 @@ def simpleInstantiationMapper(param,templateName,params):
("interactiveStrategy","cooperativeGR1Strategy"),

# Compute Invariants
("computeInvariants","computeInvariantsDontCare"),
("computeInvariants","computeInvariantsBeMoreStrict"),

# Misc
("IROSfastslow","extractExplicitPermissiveStrategy"),
Expand Down Expand Up @@ -249,7 +249,7 @@ def simpleInstantiationMapper(param,templateName,params):
("extractExplicitPermissiveStrategy","cooperativeGR1Strategy"),
("twoDimensionalCost","cooperativeGR1Strategy"),

] + combineWithAllOtherParameters("computeIncompleteInformationEstimator") + combineWithAllOtherParameters("computeAbstractWinningTrace") + combineWithAllOtherParameters("computeInterestingRunOfTheSystem") + combineWithAllOtherParameters("analyzeSafetyLivenessInteraction") + combineWithAllOtherParameters("analyzeAssumptions") + combineWithAllOtherParameters("computeCNFFormOfTheSpecification") + combineWithAllOtherParameters("analyzeInterleaving") + combineWithAllOtherParametersBut("analyzeInitialPositions",["restrictToReachableStates"]) + combineWithAllOtherParametersBut("restrictToReachableStates",["analyzeInitialPositions"]) + combineWithAllOtherParametersBut("nonDeterministicMotion",["sysInitRoboticsSemantics","interactiveStrategy","extractExplicitPermissiveStrategy","simpleSymbolicStrategy","symbolicStrategy","nonDeterministicMotionSelfLoopLivenessAssumption"]) + combineWithAllOtherParametersBut("nonDeterministicMotionSelfLoopLivenessAssumption",["sysInitRoboticsSemantics","interactiveStrategy","extractExplicitPermissiveStrategy","simpleSymbolicStrategy","symbolicStrategy","nonDeterministicMotion"]) + combineWithAllOtherParameters("computeWeakenedSafetyAssumptions") + combineWithAllOtherParameters("synthesisProfiling") + combineWithAllOtherParametersBut("environmentFriendlyStrategy",["useHeuristic","jsonOutput"]) + combineWithAllOtherParametersBut("environmentFriendlySynthesis",["useHeuristic"]) + combineWithAllOtherParametersBut("useHeuristic",["environmentFriendlySynthesis","environmentFriendlyStrategy","jsonOutput"]) + combineWithAllOtherParametersBut("computeInvariants",["computeInvariantsDontCare"]) + combineWithAllOtherParametersBut("computeInvariantsDontCare",["computeInvariants"])
] + combineWithAllOtherParameters("computeIncompleteInformationEstimator") + combineWithAllOtherParameters("computeAbstractWinningTrace") + combineWithAllOtherParameters("computeInterestingRunOfTheSystem") + combineWithAllOtherParameters("analyzeSafetyLivenessInteraction") + combineWithAllOtherParameters("analyzeAssumptions") + combineWithAllOtherParameters("computeCNFFormOfTheSpecification") + combineWithAllOtherParameters("analyzeInterleaving") + combineWithAllOtherParametersBut("analyzeInitialPositions",["restrictToReachableStates"]) + combineWithAllOtherParametersBut("restrictToReachableStates",["analyzeInitialPositions"]) + combineWithAllOtherParametersBut("nonDeterministicMotion",["sysInitRoboticsSemantics","interactiveStrategy","extractExplicitPermissiveStrategy","simpleSymbolicStrategy","symbolicStrategy","nonDeterministicMotionSelfLoopLivenessAssumption"]) + combineWithAllOtherParametersBut("nonDeterministicMotionSelfLoopLivenessAssumption",["sysInitRoboticsSemantics","interactiveStrategy","extractExplicitPermissiveStrategy","simpleSymbolicStrategy","symbolicStrategy","nonDeterministicMotion"]) + combineWithAllOtherParameters("computeWeakenedSafetyAssumptions") + combineWithAllOtherParameters("synthesisProfiling") + combineWithAllOtherParametersBut("environmentFriendlyStrategy",["useHeuristic","jsonOutput"]) + combineWithAllOtherParametersBut("environmentFriendlySynthesis",["useHeuristic"]) + combineWithAllOtherParametersBut("useHeuristic",["environmentFriendlySynthesis","environmentFriendlyStrategy","jsonOutput"]) + combineWithAllOtherParametersBut("computeInvariants",["computeInvariantsBeMoreStrict"]) + combineWithAllOtherParametersBut("computeInvariantsBeMoreStrict",["computeInvariants"])

# Which ones require (one of) another parameter(s)
requiredParameters = [
Expand All @@ -258,7 +258,7 @@ def simpleInstantiationMapper(param,templateName,params):
("jsonOutput",["explicitStrategy","environmentFriendlyStrategy"]),
("nonDeterministicMotionSelfLoopLivenessAssumption",["nonDeterministicMotion"]),
("useHeuristic",["environmentFriendlySynthesis","environmentFriendlyStrategy"]),
("computeInvariantsDontCare",["computeInvariants"]),
("computeInvariantsBeMoreStrict",["computeInvariants"]),
]

# -------------------------------------------------------
Expand Down Expand Up @@ -414,10 +414,10 @@ def permissiveStrat(params):

# Compute Invariants
def computeInvariants(params):
dontCare = "computeInvariantsDontCare" in params
dontCare = "computeInvariantsBeMoreStrict" in params
if "computeInvariants" in params:
ret = [("XComputeInvariants","true" if dontCare else "false")]
params.difference_update(["computeInvariants","computeInvariantsDontCare"])
params.difference_update(["computeInvariants","computeInvariantsBeMoreStrict"])
return ret
return []
listOfCommandLineCombinationToClassInstantiationMappers.append(computeInvariants)
Expand Down

0 comments on commit 13218b5

Please sign in to comment.