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