Comments (6)
Hi:
SPF is available here: https://github.com/SymbolicPathFinder/jpf-symbc
Please try to run canopy with it.
Thanks.
Corina
from canopy.
Hi,
Thank you for your response. Trying with the current SPF version is the first thing I tried. To make sure I just re-cloned the SPF repository, compiled and set the site.properties file to point to the new SPF installation.
I then cloned a fresh version of canopy and tried to build it but the build fails.
The error message that I get 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
I tried to see if changing that variable from private to public would temporarily fix this and allow me to compile but it does not as I ran into other compilation errors:
-compile-main:
[javac] Compiling 132 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: non-static variable solver cannot be referenced from a static context
[javac] assert IncrementalListener.solver != null;
[javac] ^
[javac] /home/parallels/jpf/cano/src/main/edu/cmu/sv/isstac/canopy/Options.java:106: error: non-static variable solver cannot be referenced from a static context
[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
from canopy.
I also tried commenting out those lines that cause the compilation error and modified the code to never build an incremental solver.
Doing that I am able to run canopy with the current version of SPF on some of the examples.
However, I still can't use the model counting option that I am interested in.
For example, if I modify src/examples/sampling/mcts/simple2.jpf and change canopy.modelcounting.amplifyrewards
to true
, then I get the following:
Exception in thread "main" java.lang.NullPointerException
at java.lang.ProcessBuilder.start(ProcessBuilder.java:1012)
at java.lang.Runtime.exec(Runtime.java:620)
at modelcounting.utils.ProcessRunner.run(ProcessRunner.java:146)
at modelcounting.omega.OmegaExecutor.execute(OmegaExecutor.java:33)
at modelcounting.analysis.SequentialAnalyzer.omegaSimplify(SequentialAnalyzer.java:324)
at modelcounting.analysis.SequentialAnalyzer.<init>(SequentialAnalyzer.java:86)
at modelcounting.analysis.SequentialAnalyzer.<init>(SequentialAnalyzer.java:79)
at edu.cmu.sv.isstac.canopy.quantification.ModelCounterFactory.createModelCounterWithProblemSettings(ModelCounterFactory.java:143)
at edu.cmu.sv.isstac.canopy.quantification.UniformUPModelCounterDecorator.getModelCounterInstance(UniformUPModelCounterDecorator.java:74)
at edu.cmu.sv.isstac.canopy.quantification.UniformUPModelCounterDecorator.countPointsOfPC(UniformUPModelCounterDecorator.java:170)
at edu.cmu.sv.isstac.canopy.quantification.ModelCountingPathQuantifier.quantifyPath(ModelCountingPathQuantifier.java:53)
at edu.cmu.sv.isstac.canopy.search.SamplingAnalysisListener.pathTerminated(SamplingAnalysisListener.java:163)
at edu.cmu.sv.isstac.canopy.search.BacktrackingSamplingSearch.search(BacktrackingSamplingSearch.java:224)
at gov.nasa.jpf.JPF.run(JPF.java:613)
at edu.cmu.sv.isstac.canopy.SamplingAnalysis.run(SamplingAnalysis.java:270)
at edu.cmu.sv.isstac.canopy.mcts.MCTSShell.start(MCTSShell.java:63)
at gov.nasa.jpf.tool.RunJPF.main(RunJPF.java:108)
Could you maybe provide the source code that was used to generate the mclib-1.0.0.jar file? How do I configure the Model Counting part to point to my LattE installation?
Thank you again for looking into this.
Regards,
Jason
from canopy.
I have decompiled the mclib jar file and looked at the code. As far as I understood there was no obvious reason for the exception that occurred when I tried to instantiate a Model Counting PathQuatifier.
In the README you mention that model counting is experimental, what do you mean by that?
Could you tell me the configuration options necessary to run canopy with model counting?
Apart from setting canopy.modelcounting.amplifyrewards
to true
, what is the rest of the settings I need to set? I guess there must be an option to specify the /path/to/LattE
and possibly other utilities.
Regards,
Jason
from canopy.
from canopy.
Thank you Kasper for your explanation, I got canopy working with Model Counting (LattE).
I might look into replacing LattE with Green or just adding the option. That could possibly give it a boost in performance.
Regards,
Jason
from canopy.
Related Issues (2)
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
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.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from canopy.