DFTRES finds "not-obviously-spurious nondeterminism" on the bitcoin-attack.txt (JANI) model file.
After reporting this and exiting gracefully, printing "Total time" and all, the JVM hangs forever in the waitForReferencePendingList Java method. The offending command is
DFTRES finds "not-obviously-spurious nondeterminism" on the bitcoin-attack.txt (JANI) model file. After reporting this and exiting gracefully, printing "Total time" and all, the JVM hangs forever in the
waitForReferencePendingList
Java method. The offending command is