Coder Social home page Coder Social logo

canopy's People

Contributors

corinus avatar jasonpap avatar ksluckow avatar qsphan avatar

Stargazers

avatar avatar avatar avatar avatar avatar

Watchers

avatar avatar avatar avatar avatar avatar avatar

Forkers

ksluckow jasonpap

canopy's Issues

Model Counting not working

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:

  1. The container has only jar files for canopy, SPF and JPF so I am not able to extend/modify that version of the code.
  2. When I change one of the example .jpf files to add the option 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

Compiling Canopy with current SPF fails

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.

  1. How different are the two versions of SPF?
  2. Which version is the latest and should be used?

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:

  1. Change the Incremental solver from private to public static
  2. and define the reset() function

While 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.

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google ❤️ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.