search

cl-unrc-lab / PhilStone

A Tool for Synthesis of Distributed Programs
0 stars 0 forks source link

Class creation and running #1

Open Sachitkothari opened 1 year ago

Sachitkothari commented 1 year ago
  1. Creation of classes on compiling did not happen in bin as specified in readme but rather in a new folder build
  2. Running the example commands gives: Error: Unable to initialize main class PS.PhilStone Caused by: java.lang.NoClassDefFoundError: java_cup/runtime/Scanner

Which can be fixed by using:

java -cp .:/home/sachit/Downloads/PhilStone/jar/java-cup-11a-runtime.jar:../jar/ST-4.0.8.jar:../jar/JFlex.jar:../jar/java-cup-11a.jar:../jar/alloy4.2.jar:../jar/freemarker.jar:../jar/dCTL_checker.jar PS.PhilStone -scope=6 ../examples/mutex/mutex3.spec

Which provides:

Exception in thread "main" java.lang.RuntimeException: Wrong Type Variable Detected in Model Checking at LTS.LTS.toMCProcess(LTS.java:835) at PS.CounterExampleSearch.modelCheck(CounterExampleSearch.java:720) at PS.CounterExampleSearch.counterExampleSearch(CounterExampleSearch.java:312) at PS.CounterExampleSearch.counterExampleSearch(CounterExampleSearch.java:421) at PS.CounterExampleSearch.counterExampleSearch(CounterExampleSearch.java:421) at PS.CounterExampleSearch.startSearch(CounterExampleSearch.java:265) at PS.PhilStone.main(PhilStone.java:230)

This problem does not seem to be on my end and I am unsure of how to fix it.

pablofcastro commented 3 months ago

Hi, thanks for reporting this, the project has been inactive for a while, it seems something minor. Can you try with the branch "openSystems", probably this will work. We will update the main branch soon.