Started implementing MSS coverage verification

Author: lucasmt

TrivialSpec.cc

@@ -18,6 +18,20 @@ void TrivialSpec::forEach(function<void(BVar, const CNFClause&)> visitor) const
     visitor(_defined[i], _negDefinitions[i]);
 }
 
+Set<BVar> TrivialSpec::eval(const Set<BVar>& assignment) const
+{
+	Set<BVar> outputAssignment;
+
+	forEach([&] (BVar var, const CNFClause& negDefinition)
+	{
+		/* Add output variable to the assignment if the negation of its definition evaluates to false */
+		if (!negDefinition.eval(assignment))
+			outputAssignment.insert(var);
+	});
+	
+	return outputAssignment;        
+}
+
 Graph<size_t> TrivialSpec::conflictGraph() const
 {
   /* Maps every x literal to the indices of the clauses where it appears. */

TrivialSpec.hpp

@@ -13,24 +13,29 @@
  */
 class TrivialSpec
 {
-  Vector<BVar> _defined; /**< z_1, z_2, ..., z_n */
-  Vector<CNFClause> _negDefinitions; /**< X_1, X_2, ..., X_n */
+	Vector<BVar> _defined; /**< z_1, z_2, ..., z_n */
+	Vector<CNFClause> _negDefinitions; /**< X_1, X_2, ..., X_n */
 
 public:
 
-  TrivialSpec(Vector<BVar> defined, Vector<CNFClause> negDefinitions);
+	TrivialSpec(Vector<BVar> defined, Vector<CNFClause> negDefinitions);
 
-  /**
-   * Iterates over definitions, executing the visitor function for each.
-   * Example: For a definition of the form (z <-> ~(l_1 | ... | l_k)),
-   * the inputs given to the visitor would be (z, (l_1, ..., l_k)).
-   */
-  void forEach(std::function<void(BVar, const CNFClause&)> visitor) const;
+	/**
+	 * Iterates over definitions, executing the visitor function for each.
+	 * Example: For a definition of the form (z <-> ~(l_1 | ... | l_k)),
+	 * the inputs given to the visitor would be (z, (l_1, ..., l_k)).
+	 */
+	void forEach(std::function<void(BVar, const CNFClause&)> visitor) const;
 
-  /**
-   * Returns graph where:
-   * - Vertex i represents clause X_i;
-   * - There is an edge between two vertices iff the clauses have opposite literals.
-   */
-  Graph<size_t> conflictGraph() const;
+	/**
+	 * Returns graph where:
+	 * - Vertex i represents clause X_i;
+	 * - There is an edge between two vertices iff the clauses have opposite literals.
+	 */
+	Graph<size_t> conflictGraph() const;
+
+	/**
+	 * Evaluates the function given by the specification on an assignment to the input variables.
+	 */
+	Set<BVar> eval(const Set<BVar>& assignment) const;
 };

Verifier.cc

@@ -62,6 +62,114 @@ bool Verifier::VerifyList()
     return true;
 }
 
-//bool VerifyInputCover();
+bool forAllAssignments(Set<BVar>& fixed,
+                       Set<BVar>& remaining,
+                       function<bool(const Set<BVar>&) callback)
+{
+	if (remaining.empty())
+	{
+		return callback(fixed);
+	}
+	else
+	{
+		BVar pivot = *remaining.begin();
+
+		remaining.erase(remaining.begin());
+
+		bool result = forAllAssignments(fixed, remaining, callback);
+
+		if (result)
+		{
+			fixed.insert(pivot);
+
+			result = forAllAssignments(fixed, remaining, callback);
+
+			fixed.erase(fixed.find(pivot));
+		}
+
+		remaining.insert(pivot);
+
+		return result;
+	}
+}
+
+bool VerifyInputCover() const
+{
+	Set<BVar> inputVars = f.inputVars();
+	Set<BVar> potentialAssignment;
+
+	forAllAssignments(inputVars, potentialAssignment,
+	                  [&f1] (const Set<BVar>& assignment) {
+		                  
+}
+
+/**
+ * Uses the given RNG to select a random subset of the given set of variables.
+ */
+Set<BVar> randomSubset(const Set<BVar>& vars,
+                       const mt19937& rng)
+{
+	/* Generates booleans with equal probability */
+	bernoulli_distribution dist(0.5);
+
+	Set<BVar> subset;
+
+	for (BVar var : vars)
+	{
+		if (dist(rng))
+			subset.insert(var);
+	}
 
-//bool RandomVerifyInputCover();
+	return subset;
+}
+
+
+
+bool RandomVerifyInputCover() const
+{
+	cout << "=== Verifying coverage ===" << endl;
+
+	/* Initialize random generation */
+	random_device rd;
+	mt19937 rng(rd());
+
+	size_t sampleSize = 100; // number of sample assignments taken
+	bool ok = true; // is set to false when verification fails
+
+	for (size_t i = 0; i < sampleSize; i++)
+	{
+		/* Generates random assignment to the x variables */
+		Set<BVar> inputAssignment = randomSubset(f.inputVars(), rng);
+
+		cout << "Random input: ";
+		print(inputAssignment, "x");
+		cout << endl;
+
+		/* Set of z variables activated by the given input */
+		Set<BVar> outputAssignment = f1.eval(inputAssignment);
+
+		cout << "Activated variables: ";
+		print(outputAssignment, "z");
+		cout << endl;
+
+		bool inputIsCovered = false;
+
+		/* Look for an MSS that covers the assignment */
+		for (const Set<BVar>& mss : mssList)
+		{
+			if (isSubset(outputAssignment, mss))
+			{
+				cout << "MSS covering this input: ";
+				print(setDifference(mss, spec.outputVars()), "z"); // remove y variables from MSS for printing
+				cout << endl;
+
+				inputIsCovered = true;
+				break;
+			}
+		}
+
+		ok &= inputIsCovered;
+	}
+
+	return ok;
+}

Verifier.hpp

@@ -54,7 +54,7 @@ Verifier(Vector<Set<BVar>> mssList, CNFSpec f);
 //The following method verify that each MSS is set to the correct assignment. It does it as follows: for every pair <M,a> of <MSS,assignment> in the list the method checks that the assignment satisfies the clauses in the MSS.
 bool VerifyList();
 
-//bool VerifyInputCover();
+bool VerifyInputCover();
 
-//bool RandomVerifyInputCover();
-};
+bool RandomVerifyInputCover();
+};