isstac / canopy Goto Github PK
View Code? Open in Web Editor NEWLicense: MIT License
License: MIT License
Hello,
I have tried canopy and looking to modify it but I need the Model Counting to work and currently it does not. So far I've only been able to run canopy in the docker container from here.
Problems with the version in the docker container:
canopy.modelcounting.amplifyrewards=true
then canopy crashes. Using the stacktrace I have traced the point of failure at the creation of the model counter (in createModelCounterWithProblemSettings
) but then the trace continues in modelcounting.analysis.SequentialAnalyzer
that is inside the mclib-1.0.0.jar file that I can't look at.I noticed that the docker container does not install any model counter (LattE/Barvinok) and the model counting jar might expect those at some path and when not able to find them canopy crashes.
Could you please provide a working implementation of canopy with Model Counting and preferably share all the code (version of SPF and JPF to checkout) as well as what other tools (LattE/Barvinok) are needed?
Thank you in advance,
Jason
The current versions of canopy and SPF are not compatible, the building of canopy fails with a fresh installation of JPF+SPF. The problem is located in the incremental solver class.
The compiler error is the following:
-compile-main:
[mkdir] Created dir: /home/parallels/jpf/cano/build/main
[javac] Compiling 138 source files to /home/parallels/jpf/cano/build/main
[javac] /home/parallels/jpf/cano/src/main/edu/cmu/sv/isstac/canopy/Options.java:105: error: solver has private access in IncrementalListener
[javac] assert IncrementalListener.solver != null;
[javac] ^
[javac] /home/parallels/jpf/cano/src/main/edu/cmu/sv/isstac/canopy/Options.java:106: error: solver has private access in IncrementalListener
[javac] IncrementalListener.solver.reset();
[javac] ^
[javac] /home/parallels/jpf/cano/src/main/edu/cmu/sv/isstac/canopy/Options.java:106: error: cannot find symbol
[javac] IncrementalListener.solver.reset();
[javac] ^
[javac] symbol: method reset()
[javac] location: variable solver of type IncrementalSolver
[javac] 3 errors
BUILD FAILED
In order to make Canopy work with the current SPF version I decompiled the SPF jar found in the docker container from here and it looks quite different with the current version of SPF that can be found on Github. I can’t do a normal diff
because the decompiled code is different from the source but I did find the difference with regard to the incremental listener that caused the Canopy compile to fail.
Based on the differences of the two versions and the compiler error messages I got I modified a fresh copy of SPF to be able to work with Canopy.
Here is the git diff
between the Github SPF and the one I got working with Canopy:
diff --git a/src/main/gov/nasa/jpf/symbc/numeric/solvers/IncrementalListener.java b/src/main/gov/nasa/jpf/symbc/numeric/solvers/IncrementalListener.java
index 2f901bb..bc2a95e 100644
--- a/src/main/gov/nasa/jpf/symbc/numeric/solvers/IncrementalListener.java
+++ b/src/main/gov/nasa/jpf/symbc/numeric/solvers/IncrementalListener.java
@@ -27,7 +27,8 @@ import gov.nasa.jpf.symbc.numeric.PCChoiceGenerator;
public class IncrementalListener extends PropertyListenerAdapter {
- private IncrementalSolver solver;
+ // private IncrementalSolver solver;
+ public static IncrementalSolver solver;
public IncrementalListener(Config config, JPF jpf) {
String stringDp = SymbolicInstructionFactory.dp[0];
diff --git a/src/main/gov/nasa/jpf/symbc/numeric/solvers/IncrementalSolver.java b/src/main/gov/nasa/jpf/symbc/numeric/solvers/IncrementalSolver.java
index 12fe422..88bf69c 100644
--- a/src/main/gov/nasa/jpf/symbc/numeric/solvers/IncrementalSolver.java
+++ b/src/main/gov/nasa/jpf/symbc/numeric/solvers/IncrementalSolver.java
@@ -20,4 +20,5 @@ package gov.nasa.jpf.symbc.numeric.solvers;
public interface IncrementalSolver {
public void push();
public void pop();
+ public void reset();
}
diff --git a/src/main/gov/nasa/jpf/symbc/numeric/solvers/ProblemZ3BitVectorIncremental.java b/src/main/gov/nasa/jpf/symbc/numeric/solvers/ProblemZ3BitVectorIncremental.java
index 9cf21f4..61978b8 100644
--- a/src/main/gov/nasa/jpf/symbc/numeric/solvers/ProblemZ3BitVectorIncremental.java
+++ b/src/main/gov/nasa/jpf/symbc/numeric/solvers/ProblemZ3BitVectorIncremental.java
@@ -102,6 +102,11 @@ public class ProblemZ3BitVectorIncremental extends ProblemGeneral implements Inc
solver.pop();
}
+ @Override^M
+ public void reset() {^M
+ solver.reset();^M
+ }^M
+^M
public void cleanup() {
// nothing to be done here
}
diff --git a/src/main/gov/nasa/jpf/symbc/numeric/solvers/ProblemZ3Incremental.java b/src/main/gov/nasa/jpf/symbc/numeric/solvers/ProblemZ3Incremental.java
index baf5883..d295c3b 100644
--- a/src/main/gov/nasa/jpf/symbc/numeric/solvers/ProblemZ3Incremental.java
+++ b/src/main/gov/nasa/jpf/symbc/numeric/solvers/ProblemZ3Incremental.java
@@ -89,6 +89,12 @@ public class ProblemZ3Incremental extends ProblemGeneral implements IncrementalS
}
+ @Override
+ public void reset() {
+ solver.reset();
+
+ }
+
public void cleanup() {
// nothing to be done here
}
It’s two things:
private
to public static
reset()
functionWhile this makes canopy work for now, how do you think this should be handled?
It would be better if the change was made in canopy rather than SPF but I don’t know the code well enough to do it. On the other hand, if the SPF.jar file that include also the changes I made is a newer, more complete, version of SPF you could push that to the public repository.
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.