Back
session BoundedBufferFullToNonFullAssertionSlice {
source = "CompleteBoundedBuffer.java"
classpath = "."
included = ""
output = "BoundedBufferFullToNonFullAssertionSlice"
directory = "."
description = "none"
components = "Slicer+Checker"
specification = "BoundedBuffer.specification"
temporal = "FullToNonFull"
assertion = "PositiveBoundAndPost"
abstraction = ""
babs = ""
birc = ""
spin = "-DMEMCNT=31 -DVECTORSZ=1024 -DNOREDUCE+-n -m10000 -w18 -a -e"
}
session BoundedBufferIndexRangeSlice {
source = "CompleteBoundedBuffer.java"
classpath = "."
included = ""
output = "BoundedBufferIndexRangeAssertionSlice"
directory = "."
description = "none"
components = "Slicer+Checker"
specification = "BoundedBuffer.specification"
temporal = "IndexRange"
assertion = ""
abstraction = ""
babs = ""
birc = ""
spin = "-DMEMCNT=31 -DVECTORSZ=1024 -DNOREDUCE+-n -m10000 -w18 -a -e"
}
session Deadlock {
source = "Deadlock.java"
classpath = "."
included = ""
output = "Deadlock"
directory = "."
description = "none"
components = "Checker"
specification = ""
temporal = ""
assertion = ""
abstraction = ""
babs = ""
birc = ""
spin = "-DMEMCNT=31 -DVECTORSZ=1024 -DNOREDUCE+-n -m10000 -w18 -a -e"
}
session DeadlockPoint {
source = "Deadlock.java"
classpath = "."
included = ""
output = "DealockPoint"
directory = "."
description = "none"
components = "BABS+Checker"
specification = ""
temporal = ""
assertion = ""
abstraction = "Deadlock.abstraction"
babs = ""
birc = ""
spin = "-DMEMCNT=31 -DVECTORSZ=1024 -DNOREDUCE+-n -m10000 -w18 -a -e"
}
session DeadlockSlice {
source = "Deadlock.java"
classpath = "."
included = ""
output = "DeadlockSlice"
directory = "."
description = "none"
components = "Slicer+Checker"
specification = ""
temporal = ""
assertion = ""
abstraction = ""
babs = ""
birc = ""
spin = "-DMEMCNT=31 -DVECTORSZ=1024 -DNOREDUCE+-n -m10000 -w18 -a -e"
}
session NestedDeadlock {
source = "NestedMonitorDeadlock.java"
classpath = "."
included = ""
output = "default"
directory = "."
description = "none"
components = "Checker"
specification = ""
temporal = ""
assertion = ""
abstraction = ""
babs = ""
birc = ""
spin = "-DMEMCNT=31 -DVECTORSZ=1024 -DNOREDUCE+-n -m10000 -w18 -a -e"
}
session NestedDeadlockSlice {
source = "NestedMonitorDeadlock.java"
classpath = "."
included = ""
output = "NestedDeadlockSlice"
directory = "."
description = "none"
components = "Slicer+Checker"
specification = ""
temporal = ""
assertion = ""
abstraction = ""
babs = ""
birc = ""
spin = "-DMEMCNT=31 -DVECTORSZ=1024 -DNOREDUCE+-n -m10000 -w18 -a -e"
}
session PipeIntStage1Signs {
source = "PipeInt.java"
classpath = "."
included = ""
output = "PipeIntStage1Signs"
directory = "."
description = "none"
components = "BABS+Checker"
specification = "PipeInt.specification"
temporal = "stage1ShutdownProp"
assertion = ""
abstraction = "PipeInt.abstraction"
babs = ""
birc = ""
spin = "-DMEMCNT=31 -DVECTORSZ=1024 -DNOREDUCE+-n -m10000 -w18 -a -e"
}
Back