Unable to run the example

[czheo]

I tried to run the example on README.md with the command below.

sbt -Djava.library.path=lib/c4/build/src/libc4/:lib/z3/build/z3-dist/lib/ "run-main edu.berkeley.cs.boom.molly.SyncFTChecker \
    src/test/resources/examples_ft/delivery/simplog.ded \
    src/test/resources/examples_ft/delivery/deliv_assert.ded \
    --EOT 4 \
    --EFF 2 \
    --nodes a,b,c \
    --crashes 0 \
    --prov-diagrams"

My OS X blamed me with errors.

[error] (run-main-0) java.lang.NumberFormatException: For input string: "java/lang/ClassNotFoundExceptionava/lang/NoSunjava/lang/NoSuchMethodException"
java.lang.NumberFormatException: For input string: "java/lang/ClassNotFoundExceptionava/lang/NoSunjava/lang/NoSuchMethodException"
    at java.lang.NumberFormatException.forInputString(NumberFormatException.java:48)
    at java.lang.Integer.parseInt(Integer.java:449)
    at java.lang.Integer.parseInt(Integer.java:499)
    at scala.collection.immutable.StringLike$class.toInt(StringLike.scala:272)
    at scala.collection.immutable.StringOps.toInt(StringOps.scala:30)
    at edu.berkeley.cs.boom.molly.UltimateModel$$anonfun$tableAtTime$1.apply(UltimateModel.scala:12)
    at edu.berkeley.cs.boom.molly.UltimateModel$$anonfun$tableAtTime$1.apply(UltimateModel.scala:12)
    at scala.collection.TraversableLike$$anonfun$filterImpl$1.apply(TraversableLike.scala:259)
    at scala.collection.immutable.List.foreach(List.scala:381)
    at scala.collection.TraversableLike$class.filterImpl(TraversableLike.scala:258)
    at scala.collection.TraversableLike$class.filter(TraversableLike.scala:270)
    at scala.collection.AbstractTraversable.filter(Traversable.scala:104)
    at edu.berkeley.cs.boom.molly.UltimateModel.tableAtTime(UltimateModel.scala:12)
    at edu.berkeley.cs.boom.molly.Verifier.<init>(Verifier.scala:74)
    at edu.berkeley.cs.boom.molly.SyncFTChecker$.check(SyncFTChecker.scala:78)
    at edu.berkeley.cs.boom.molly.SyncFTChecker$$anonfun$main$2.apply(SyncFTChecker.scala:105)
    at edu.berkeley.cs.boom.molly.SyncFTChecker$$anonfun$main$2.apply(SyncFTChecker.scala:102)
    at scala.Option.map(Option.scala:146)
    at edu.berkeley.cs.boom.molly.SyncFTChecker$.main(SyncFTChecker.scala:102)
    at edu.berkeley.cs.boom.molly.SyncFTChecker.main(SyncFTChecker.scala)
    at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
    at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:39)
    at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:25)
    at java.lang.reflect.Method.invoke(Method.java:597)

Any idea about this?

[KamalaRamas]

Hi,

This looks like a java language exception and I am not sure what caused it. Does running sbt "run-main edu.berkeley.cs.boom.molly.SyncFTChecker"

display the usage details?

[at15]

@czheo I have it up and running on my ubuntu machine. Have you got c4 and z3 compiled in the lib folder (git submodule init & update works for c4 but does not work for Z3, so I clone z3 and run make z3) and what's your java and scala version?

My Java & Scala version

Scala compiler version 2.11.8 -- Copyright 2002-2016, LAMP/EPFL
java version "1.8.0_101"
Java(TM) SE Runtime Environment (build 1.8.0_101-b13)
Java HotSpot(TM) 64-Bit Server VM (build 25.101-b13, mixed mode)

[czheo]

It seems caused by old Java version. Fixed after I updated Java 6 to 8. @KamalaRamas @at15 Thx!