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" }