SimpleDBのテストの実行(成功)+モデル検査(失敗)

テストを実行する

code: result.txt

+braun+e205723 java -cp build/classes/java/main simpledb.tx.ConcurrencyTest

Tx B: request xlock 2

Tx A: request slock 1

Tx B: receive xlock 2

Tx A: receive slock 1

Tx C: request xlock 1

Tx B: request slock 1

Tx A: request slock 2

Tx B: receive slock 1

transaction 2 committed

Tx B: commit

Tx A: receive slock 2

transaction 1 committed

Tx A: commit

Tx C: receive xlock 1

Tx C: request slock 2

Tx C: receive slock 2

transaction 3 committed

Tx C: commit

PathFinderでモデル検査を実行する

失敗

code: result.txt

+braun+e205723 /opt/jpf-core/bin/jpf +classpath=build/classes/java/main simpledb.tx.ConcurrencyTest

JavaPathfinder core system v8.0 (rev 1a704e1d6c3d92178504f8cdfe57b068b4e22d9c) - (C) 2005-2014 United States Government. All rights reserved.

====================================================== system under test

simpledb.tx.ConcurrencyTest.main()

====================================================== search started: 1/22/24, 6:32 AM

====================================================== error 1

gov.nasa.jpf.vm.NoUncaughtExceptionsProperty

java.lang.NoSuchMethodError: java.io.RandomAccessFile.write([B)V

at simpledb.file.FileMgr.append(FileMgr.java:56)

at simpledb.log.LogMgr.appendNewBlock(LogMgr.java:91)

at simpledb.log.LogMgr.<init>(LogMgr.java:35)

at simpledb.server.SimpleDB.<init>(SimpleDB.java:38)

at simpledb.tx.ConcurrencyTest.main(ConcurrencyTest.java:15)

thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}

owned locks:simpledb.file.FileMgr@209

call stack:

at simpledb.file.FileMgr.append(FileMgr.java:56)

at simpledb.log.LogMgr.appendNewBlock(LogMgr.java:91)

at simpledb.log.LogMgr.<init>(LogMgr.java:35)

at simpledb.server.SimpleDB.<init>(SimpleDB.java:38)

at simpledb.tx.ConcurrencyTest.main(ConcurrencyTest.java:15)

====================================================== results

====================================================== statistics

elapsed time: 00:00:00

states: new=1,visited=0,backtracked=0,end=0

search: maxDepth=1,constraints=0

choice generators: thread=1 (signal=0,lock=1,sharedRef=0,threadApi=0,reschedule=0), data=0

heap: new=788,released=0,maxLive=0,gcCycles=0

instructions: 14887

max memory: 1024MB

loaded code: classes=117,methods=2674

====================================================== search finished: 1/22/24, 6:32 AM