Storm.ddbisim

Benchmark
Model:echoring v.1 (MDP)
Parameter(s)ITERATIONS = 100
Property:MaxOffline1 (prob-reach)
Invocation (ddbisim)
/home/tq429871/storm/build/bin/storm --jani /rwthfs/rz/cluster/home/tq429871/git/storm-qcomp-benchmarks/qcomp/benchmarks/mdp/echoring/echoring.jani --janiproperty MaxOffline1 --constants ITERATIONS=100 --engine dd-to-sparse --bisimulation --sylvan:maxmem 4096 --sylvan:threads 4 --timemem
Symbolic bisimulation with sparse quotient and sylvan using 4GB memory
Execution
Walltime:0.09445667266845703s
Return code:1
Log
Storm 1.6.2

Date: Sat Sep  5 20:53:12 2020
Command line arguments: --jani /rwthfs/rz/cluster/home/tq429871/git/storm-qcomp-benchmarks/qcomp/benchmarks/mdp/echoring/echoring.jani --janiproperty MaxOffline1 --constants ITERATIONS=100 --engine dd-to-sparse --bisimulation '--sylvan:maxmem' 4096 '--sylvan:threads' 4 --timemem
Current working directory: /rwthfs/rz/cluster/home/tq429871/git/storm-qcomp-benchmarks

Time for model input parsing: 0.033s.

 WARN (cli.cpp:262): The model checking query does not seem to be supported for the selected engine. Storm will try to solve the query, but you will most likely get an error for at least one of the provided properties.
ERROR (DdJaniModelBuilder.cpp:2138): The symbolic JANI model builder currently does not support assignment levels.
ERROR (storm.cpp:23): An exception caused Storm to terminate. The message of the exception is: WrongFormatException: The symbolic JANI model builder currently does not support assignment levels.