Model Counting not working about canopy

[corinus]

Hi:
SPF is available here: https://github.com/SymbolicPathFinder/jpf-symbc
Please try to run canopy with it.
Thanks.
Corina

[JasonPap]

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

[JasonPap]

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

[JasonPap]

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

[ksluckow]

Thanks for your interest, Jason. We are currently figuring out how the model counting part can be distributed with canopy. In the meantime, I can give you access to the src of mclib. The model counting integration in Canopy was used for experimenting with weighted sampling. It worked well for those purposes. We didn't fully evaluate this direction, but the throughput of samples was many times slower than unweighted sampling due to the cost of performing model counting. It is likely this can be improved though. I believe you can set the omega and latte paths with the jpf configs: canopy.modelcounting.omegaPath canopy.modelcounting.lattePath In addition, for each application jpf file, you will have to specify canopy.modelcounting.problemsettings which should be assigned the path to a file that describe the domain of the input parameters and the usage profile. You can see an example in src/examples/sampling/mcts/quicksort.up which is referred to in src/examples/sampling/mcts/QuickSort.jpf Hope this helps. Cheers, Kasper

…

On Thu, 2 Aug 2018 at 05:54 Jason Papapanagiotakis ***@***.***> wrote: 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 — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#1 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AD_M2g7pwFJ0H-l7UAOvsb6blCSL_9Itks5uMvaKgaJpZM4VmR9B> .

[JasonPap]

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