gov.nasa.jpf.util.test

Class TestMultiProcessJPF

java.lang.Object

gov.nasa.jpf.util.test.TestJPF

gov.nasa.jpf.util.test.TestMultiProcessJPF

All Implemented Interfaces:

JPFShell

public abstract class TestMultiProcessJPF
extends TestJPF

Author:

Nastaran Shafiei This is a root class for testing multi-processes code. This forces JPF to use MultiProcessVM and DistributedSchedulerFactory

Field Summary

Fields inherited from class gov.nasa.jpf.util.test.TestJPF

globalRunDirectly, globalShowConfig, hideSummary, runDirectly, SAME_PACKAGE, showConfig, showConfigSources, stopOnFailure, sutClassName, UNNAMED_PACKAGE

Constructor Summary

Constructors

Constructor and Description
TestMultiProcessJPF()

Method Summary

Methods

Modifier and Type	Method and Description
protected int	getProcessId()
protected boolean	mpVerifyAssertionError(int prcNum, String... args)
protected boolean	mpVerifyAssertionErrorDetails(int prcNum, String details, String... args)
protected boolean	mpVerifyDeadlock(int prcNum, String... args)
protected boolean	mpVerifyJPFException(int prcNum, TypeRef xClsSpec, String... args)
protected boolean	mpVerifyNoPropertyViolation(int prcNum, String... args)
protected boolean	mpVerifyPropertyViolation(int prcNum, TypeRef propertyClsSpec, String... args)
protected boolean	mpVerifyUnhandledException(int prcNum, String xClassName, String... args)
protected boolean	mpVerifyUnhandledExceptionDetails(int prcNum, String xClassName, String details, String... args)
protected void	setTestTargetKeys(Config conf, StackTraceElement testMethod)

Methods inherited from class gov.nasa.jpf.util.test.TestJPF

assertArrayEquals, assertEquals, assertEquals, assertEquals, assertEquals, assertEquals, assertEquals, assertEquals, assertEquals, assertEquals, assertEquals, assertEquals, assertEquals, assertEquals, assertEquals, assertFalse, assertFalse, assertionError, assertionError, assertionErrorDetails, assertionErrorDetails, assertNotNull, assertNotNull, assertNull, assertNull, assertSame, assertSame, assertTrue, assertTrue, createAndRunJPF, createJPF, deadlock, fail, fail, fail, getAfterClassMethods, getAfterMethods, getBeforeClassMethods, getBeforeMethods, getCaller, getContextMethods, getGlobalArgs, getMatchingMethods, getOptions, getSutClassName, getTestMethods, hasExplicitTestMethods, isJPFRun, isJUnitRun, isMatchingMethod, isRunTestRun, jpfException, jpfException, noPropertyViolation, noPropertyViolation, propertyViolation, propertyViolation, report, reportResults, reportTestCleanup, reportTestFinished, reportTestInitialization, reportTestStart, runTests, runTestsOfThisClass, setTestMethod, setTestMethod, start, unhandledException, unhandledException, verifyAssertionError, verifyAssertionErrorDetails, verifyDeadlock, verifyJPFException, verifyNoPropertyViolation, verifyPropertyViolation, verifyUnhandledException, verifyUnhandledExceptionDetails

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

TestMultiProcessJPF

public TestMultiProcessJPF()

Method Detail

setTestTargetKeys

protected void setTestTargetKeys(Config conf,
                     StackTraceElement testMethod)

Overrides:

setTestTargetKeys in class TestJPF

getProcessId

protected int getProcessId()

mpVerifyAssertionErrorDetails

protected boolean mpVerifyAssertionErrorDetails(int prcNum,
                                    String details,
                                    String... args)

mpVerifyAssertionError

protected boolean mpVerifyAssertionError(int prcNum,
                             String... args)

mpVerifyNoPropertyViolation

protected boolean mpVerifyNoPropertyViolation(int prcNum,
                                  String... args)

mpVerifyUnhandledExceptionDetails

protected boolean mpVerifyUnhandledExceptionDetails(int prcNum,
                                        String xClassName,
                                        String details,
                                        String... args)

mpVerifyUnhandledException

protected boolean mpVerifyUnhandledException(int prcNum,
                                 String xClassName,
                                 String... args)

mpVerifyJPFException

protected boolean mpVerifyJPFException(int prcNum,
                           TypeRef xClsSpec,
                           String... args)

mpVerifyPropertyViolation

protected boolean mpVerifyPropertyViolation(int prcNum,
                                TypeRef propertyClsSpec,
                                String... args)

mpVerifyDeadlock

protected boolean mpVerifyDeadlock(int prcNum,
                       String... args)