Generate All Minimal Inductive Validity Cores (MIVCs)

Add option to generate all minimal inductive validity cores. Co-authored-by: Elaheh <[email protected]> Co-authored-by: Mike Whalen <[email protected]> Co-authored-by: porw1492 <[email protected]> Co-authored-by: jar-ben <[email protected]> Co-authored-by: jar-ben <[email protected]> Co-authored-by: jliu29 <[email protected]>
loonwerks · Jun 6, 2020 · a7c848c · a7c848c
1 parent d39784b
commit a7c848c
Show file tree

Hide file tree

Showing 240 changed files with 9,541 additions and 3,749 deletions.
diff --git a/README.md b/README.md
@@ -35,3 +35,19 @@ as its underlying SMT solver. Advanced users may wish to install alternative sol
 [Yices 2](http://yices.csl.sri.com/index.shtml),
 [CVC4](http://cvc4.cs.nyu.edu/web/), or
 [MathSAT](http://mathsat.fbk.eu/).
+
+Minimal IVCs enumeration (optional)
+-----------------------------------
+JKind supports enumeration of All Minimal Inductive Validity Cores (All-MIVCs) to provide a full enumeration of all minimal set of model elements necessary for the inductive proofs of a safety property. 
+Both the offline enumeration (as described in [1]) and the online enumeration (as described in [2]) have been implemented, and the offline enumeration is the algorithm made available for general use. 
+To use the MIVC enumeration, run JKind with the following arguments: 
+```
+-all_ivcs -solver z3
+```
+In addition, use the -timeout argument to limit the time for the enumeration, e.g., 
+```
+-timeout 1800
+```
+
+[1] E. Ghassabani, M. W. Whalen, and A. Gacek. Efficient generation of all minimal inductive validity cores. 2017 Formal Methods in Computer Aided Design (FMCAD), pages 31–38, 2017.
+[2] J. Bendik, E. Ghassabani, M. Whalen, and I. Cerna. Online enumeration of all minimal inductive validity cores. In International Conference on Software Engineering and Formal Methods, pages 189–204. Springer, 2018.
diff --git a/jkind-api/src/jkind/api/ApiUtil.java b/jkind-api/src/jkind/api/ApiUtil.java
@@ -37,8 +37,8 @@ public static File writeTempFile(String fileName, String fileExt, String content
 		}
 	}
 
-	public static void execute(Function<File, ProcessBuilder> runCommand, File lustreFile,
-			JKindResult result, IProgressMonitor monitor, DebugLogger debug) {
+	public static void execute(Function<File, ProcessBuilder> runCommand, File lustreFile, JKindResult result,
+			IProgressMonitor monitor, DebugLogger debug) {
 		File xmlFile = null;
 		try {
 			xmlFile = getXmlFile(lustreFile);
@@ -68,9 +68,8 @@ private static File getXmlFile(File lustreFile) {
 		return new File(lustreFile.toString() + ".xml");
 	}
 
-	private static void callJKind(Function<File, ProcessBuilder> runCommand, File lustreFile,
-			File xmlFile, JKindResult result, IProgressMonitor monitor, DebugLogger debug)
-			throws IOException, InterruptedException {
+	private static void callJKind(Function<File, ProcessBuilder> runCommand, File lustreFile, File xmlFile,
+			JKindResult result, IProgressMonitor monitor, DebugLogger debug) throws IOException, InterruptedException {
 		ProcessBuilder builder = runCommand.apply(lustreFile);
 		debug.println("JKind command: " + ApiUtil.getQuotedCommand(builder.command()));
 		Process process = null;
@@ -106,8 +105,8 @@ private static void callJKind(Function<File, ProcessBuilder> runCommand, File lu
 				monitor.done();
 
 				if (code != 0 && !monitor.isCanceled()) {
-					throw new JKindException("Abnormal termination, exit code " + code
-							+ System.lineSeparator() + result.getText());
+					throw new JKindException(
+							"Abnormal termination, exit code " + code + System.lineSeparator() + result.getText());
 				}
 			}
 
@@ -207,8 +206,7 @@ public static String readAll(InputStream inputStream) throws IOException {
 	}
 
 	public static String getQuotedCommand(List<String> pieces) {
-		return pieces.stream().map(p -> p.contains(" ") ? "\"" + p + "\"" : p)
-				.collect(joining(" "));
+		return pieces.stream().map(p -> p.contains(" ") ? "\"" + p + "\"" : p).collect(joining(" "));
 	}
 
 	public static void addEnvironment(ProcessBuilder builder, Map<String, String> environment) {

diff --git a/jkind-api/src/jkind/api/Backend.java b/jkind-api/src/jkind/api/Backend.java
@@ -1,5 +1,5 @@
 package jkind.api;
 
 public enum Backend {
-  JKIND, KIND2, SALLY
+	JKIND, KIND2, SALLY
 }
diff --git a/jkind-api/src/jkind/api/JKindApi.java b/jkind-api/src/jkind/api/JKindApi.java
@@ -8,12 +8,12 @@
 import java.util.List;
 import java.util.Map;
 
+import org.eclipse.core.runtime.IProgressMonitor;
+
 import jkind.JKindException;
 import jkind.SolverOption;
 import jkind.api.results.JKindResult;
 
-import org.eclipse.core.runtime.IProgressMonitor;
-
 /**
  * The primary interface to JKind.
  */
@@ -26,11 +26,11 @@ public class JKindApi extends KindApi {
 	protected Integer pdrMax = null;
 	protected boolean inductiveCounterexamples = false;
 	protected boolean ivcReduction = false;
+	protected boolean allIvcs = false;
 	protected boolean smoothCounterexamples = false;
 	protected boolean slicing = true;
-	
+
 	protected List<String> vmArgs = Collections.emptyList();
-
 	protected SolverOption solver = null;
 
 	protected String jkindJar;
@@ -40,7 +40,7 @@ public class JKindApi extends KindApi {
 
 	/**
 	 * Set the maximum depth for BMC and k-induction
-	 * 
+	 *
 	 * @param n
 	 *            A non-negative integer
 	 */
@@ -65,7 +65,7 @@ public void disableInvariantGeneration() {
 
 	/**
 	 * Set the maximum number of PDR instances to run
-	 * 
+	 *
 	 * @param pdrMax
 	 *            A non-negative integer
 	 */
@@ -97,6 +97,13 @@ public void setIvcReduction() {
 		ivcReduction = true;
 	}
 
+	/**
+	 * Find all inductive validity cores for valid properties
+	 */
+	public void setAllIvcs() {
+		allIvcs = true;
+	}
+
 	/**
 	 * Post-process counterexamples to have minimal input value changes
 	 */
@@ -110,7 +117,7 @@ public void setSmoothCounterexamples() {
 	public void disableSlicing() {
 		slicing = false;
 	}
-	
+
 	/**
 	 * Set VM args
 	 */
@@ -151,7 +158,7 @@ public void setWriteAdviceFile(String fileName) {
 
 	/**
 	 * Run JKind on a Lustre program
-	 * 
+	 *
 	 * @param lustreFile
 	 *            File containing Lustre program
 	 * @param result
@@ -197,6 +204,10 @@ private ProcessBuilder getJKindProcessBuilder(File lustreFile) {
 		if (ivcReduction) {
 			args.add("-ivc");
 		}
+		if (allIvcs) {
+			args.add("-all_ivcs");
+		}
+
 		if (smoothCounterexamples) {
 			args.add("-smooth");
 		}
@@ -232,7 +243,7 @@ protected String[] getJKindCommand() {
 		args.add("-jar");
 		args.add(getOrFindJKindJar());
 		args.add("-jkind");
-		
+
 		return args.toArray(new String[args.size()]);
 	}
 

diff --git a/jkind-api/src/jkind/api/JLustre2ExcelApi.java b/jkind-api/src/jkind/api/JLustre2ExcelApi.java
@@ -93,8 +93,7 @@ public File execute(File lustreFile) {
 		try {
 			process = pb.start();
 			String output = ApiUtil.readOutput(process, new NullProgressMonitor());
-			debug.println("JLustre2Excel output",
-					debug.saveFile("jlustre2excel-output-", ".txt", output));
+			debug.println("JLustre2Excel output", debug.saveFile("jlustre2excel-output-", ".txt", output));
 			return new File(lustreFile.getPath() + ".xls");
 		} catch (IOException e) {
 			throw new JKindException("Error running JLustre2Excel", e);

diff --git a/jkind-api/src/jkind/api/JRealizabilityApi.java b/jkind-api/src/jkind/api/JRealizabilityApi.java
@@ -23,7 +23,7 @@ public class JRealizabilityApi {
 	private boolean extendCounterexample = false;
 	private boolean reduce = false;
 	private DebugLogger debug = new DebugLogger();
-	
+
 	private List<String> vmArgs = Collections.emptyList();
 
 	private String jkindJar;
@@ -104,13 +104,13 @@ public void setJKindJar(String jkindJar) {
 	public void setEnvironment(String key, String value) {
 		environment.put(key, value);
 	}
-	
+
 	/**
 	 * Set VM args
 	 */
 	public void setVmArgs(List<String> args) {
 		vmArgs = new ArrayList<>(args);
-	}	
+	}
 
 	/**
 	 * Run JRealizability on a Lustre program
@@ -197,7 +197,7 @@ protected String[] getJRealizabilityCommand() {
 		args.add("-jar");
 		args.add(getOrFindJKindJar());
 		args.add("-jrealizability");
-		
+
 		return args.toArray(new String[args.size()]);
 	}
 

diff --git a/jkind-api/src/jkind/api/examples/Kind2WebExample.java b/jkind-api/src/jkind/api/examples/Kind2WebExample.java
@@ -19,8 +19,8 @@ public static void main(String[] args) throws Exception {
 		URI uri = new URI(args[0]);
 		String filename = args[1];
 
-		try (LineInputStream lines = new LineInputStream(new Kind2WebInputStream(uri,
-				getKindArgs(), getLustre(filename)))) {
+		try (LineInputStream lines = new LineInputStream(
+				new Kind2WebInputStream(uri, getKindArgs(), getLustre(filename)))) {
 			String line;
 			while ((line = lines.readLine()) != null) {
 				System.out.print(line);

diff --git a/jkind-api/src/jkind/api/examples/coverage/CoverageReporter.java b/jkind-api/src/jkind/api/examples/coverage/CoverageReporter.java
@@ -22,17 +22,16 @@
 import jkind.results.ValidProperty;
 
 public class CoverageReporter {
-	public static void writeHtml(String filename, Program program,
-			Map<String, ELocation> locationMap, JKindResult result) throws Exception {
+	public static void writeHtml(String filename, Program program, Map<String, ELocation> locationMap,
+			JKindResult result) throws Exception {
 		try (BufferedWriter writer = new BufferedWriter(new FileWriter(filename + ".html"))) {
 			writer.write("<html>\n");
 			writeHeader(writer);
 			writer.write("<body>\n");
 
 			for (PropertyResult pr : result.getPropertyResults()) {
 				if (!(pr.getProperty() instanceof ValidProperty)) {
-					writer.write("<p class='not-valid'>" + pr.getProperty().getName()
-							+ " is invalid/unknown</p>\n");
+					writer.write("<p class='not-valid'>" + pr.getProperty().getName() + " is invalid/unknown</p>\n");
 				}
 			}
 
@@ -41,13 +40,12 @@ public static void writeHtml(String filename, Program program,
 					ValidProperty vp = (ValidProperty) pr.getProperty();
 					List<String> allIvcs = getAllIvcs(program);
 
-					List<ELocation> locations = getUnusedLocations(locationMap, allIvcs,
-							vp.getIvc());
+					List<ELocation> locations = getUnusedLocations(locationMap, allIvcs, vp.getIvc());
 
 					int total = allIvcs.size();
 					int covered = total - locations.size();
-					String stats = String.format("%s: %.1f%% (%d of %d covered)", vp.getName(),
-							100.0 * covered / total, covered, total);
+					String stats = String.format("%s: %.1f%% (%d of %d covered)", vp.getName(), 100.0 * covered / total,
+							covered, total);
 					writer.write("<div class='valid'>\n");
 					writer.write("<div class='stats'>" + stats + "</div>\n");
 					displayLocations(writer, filename, locations);
@@ -60,8 +58,8 @@ public static void writeHtml(String filename, Program program,
 		}
 	}
 
-	private static List<ELocation> getUnusedLocations(Map<String, ELocation> locationMap,
-			List<String> allIvcs, Set<String> usedIvcs) {
+	private static List<ELocation> getUnusedLocations(Map<String, ELocation> locationMap, List<String> allIvcs,
+			Set<String> usedIvcs) {
 		Set<String> baseUsedIvcs = new HashSet<>();
 		Pattern pattern = Pattern.compile(".*(" + ExtractorVisitor.PREFIX + "\\d+).*");
 		for (String ivc : usedIvcs) {
@@ -101,8 +99,8 @@ private static void writeHeader(BufferedWriter writer) throws IOException {
 		writer.write("</head>\n");
 	}
 
-	private static void displayLocations(BufferedWriter writer, String filename,
-			List<ELocation> locations) throws Exception {
+	private static void displayLocations(BufferedWriter writer, String filename, List<ELocation> locations)
+			throws Exception {
 		int i = 0;
 
 		writer.write("<div class='lustre'>");

diff --git a/jkind-api/src/jkind/api/examples/coverage/Main.java b/jkind-api/src/jkind/api/examples/coverage/Main.java
@@ -26,11 +26,11 @@ public static void main(String[] args) throws Exception {
 		}
 		String filename = args[0];
 		Program program = parseLustre(new ANTLRFileStream(filename));
-		
+
 		ExtractorVisitor visitor = new ExtractorVisitor();
 		program = visitor.visit(program);
 		program = SubrangeFixVisitor.fix(program);
-		
+
 		Util.writeToFile(program.toString(), new File(filename + ".coverage"));
 		JKindResult result = runJKind(program);
 		CoverageReporter.writeHtml(filename, program, visitor.getLocationMap(), result);

diff --git a/jkind-api/src/jkind/api/results/AnalysisResult.java b/jkind-api/src/jkind/api/results/AnalysisResult.java
@@ -6,24 +6,24 @@
 public abstract class AnalysisResult {
 	protected final String name;
 	protected final PropertyChangeSupport pcs = new PropertyChangeSupport(this);
-	protected AnalysisResult parent; 
-	
+	protected AnalysisResult parent;
+
 	public AnalysisResult(String name) {
 		this.name = name;
 	}
-	
+
 	public String getName() {
 		return name;
 	}
-	
+
 	public void setParent(AnalysisResult parent) {
 		pcs.firePropertyChange("parent", this.parent, this.parent = parent);
 	}
-	
+
 	public AnalysisResult getParent() {
 		return parent;
 	}
-	
+
 	public void addPropertyChangeListener(PropertyChangeListener listener) {
 		pcs.addPropertyChangeListener(listener);
 	}

diff --git a/jkind-api/src/jkind/api/results/CompositeAnalysisResult.java b/jkind-api/src/jkind/api/results/CompositeAnalysisResult.java
@@ -26,7 +26,7 @@ private void addMultiStatus(MultiStatus other) {
 		multiStatus.add(other);
 		pcs.firePropertyChange("multiStatus", null, other);
 	}
-	
+
 	public List<AnalysisResult> getChildren() {
 		return Collections.unmodifiableList(children);
 	}
@@ -43,14 +43,14 @@ public void propertyChange(PropertyChangeEvent evt) {
 			multiStatus.add((Status) evt.getNewValue());
 			pcs.firePropertyChange("status", evt.getOldValue(), evt.getNewValue());
 		}
-		
+
 		if ("multiStatus".equals(evt.getPropertyName()) && children.contains(evt.getSource())) {
 			multiStatus.remove((MultiStatus) evt.getOldValue());
 			multiStatus.add((MultiStatus) evt.getNewValue());
 			pcs.firePropertyChange("multiStatus", evt.getOldValue(), evt.getNewValue());
 		}
 	}
-	
+
 	@Override
 	public String toString() {
 		return name + children;

diff --git a/jkind-api/src/jkind/api/results/JKindResult.java b/jkind-api/src/jkind/api/results/JKindResult.java
@@ -113,8 +113,7 @@ public JKindResult(String name, List<String> properties, List<Boolean> invertSta
 	 * @param renaming
 	 *            Renaming to apply to properties
 	 */
-	public JKindResult(String name, List<String> properties, List<Boolean> invertStatus,
-			Renaming renaming) {
+	public JKindResult(String name, List<String> properties, List<Boolean> invertStatus, Renaming renaming) {
 		super(name);
 		this.renaming = renaming;
 		addProperties(properties, invertStatus);
@@ -151,8 +150,7 @@ public PropertyResult addProperty(String property, boolean invertStatus) {
 		PropertyResult propertyResult = new PropertyResult(property, renaming, invertStatus);
 		propertyResults.add(propertyResult);
 		propertyResult.setParent(this);
-		pcs.fireIndexedPropertyChange("propertyResults", propertyResults.size() - 1, null,
-				propertyResult);
+		pcs.fireIndexedPropertyChange("propertyResults", propertyResults.size() - 1, null, propertyResult);
 		addStatus(propertyResult.getStatus());
 		propertyResult.addPropertyChangeListener(this);
 		return propertyResult;
@@ -353,8 +351,7 @@ public void propertyChange(PropertyChangeEvent evt) {
 			pcs.firePropertyChange("status", evt.getOldValue(), evt.getNewValue());
 		}
 
-		if ("multiStatus".equals(evt.getPropertyName())
-				&& propertyResults.contains(evt.getSource())) {
+		if ("multiStatus".equals(evt.getPropertyName()) && propertyResults.contains(evt.getSource())) {
 			multiStatus.remove((MultiStatus) evt.getOldValue());
 			multiStatus.add((MultiStatus) evt.getNewValue());
 			pcs.firePropertyChange("multiStatus", evt.getOldValue(), evt.getNewValue());