From a2fd0dd5b7bd594ac6d66c7681ee4dbf8d237f05 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 5 Dec 2006 10:55:11 +0000 Subject: [PATCH] Addition of F (future) and G (global) operators to property specification language. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@181 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/include/SimulatorEngine.h | 1848 ++++++++++--------- prism/include/simpctl.h | 8 +- prism/src/parser/PCTLProbBoundedFuture.java | 167 ++ prism/src/parser/PCTLProbBoundedGlobal.java | 167 ++ prism/src/parser/PCTLProbFuture.java | 57 + prism/src/parser/PCTLProbGlobal.java | 57 + prism/src/parser/PrismParser.java | 1758 ++++++++++-------- prism/src/parser/PrismParser.jj | 67 +- prism/src/prism/NondetModelChecker.java | 114 +- prism/src/prism/ProbModelChecker.java | 58 +- prism/src/prism/StochModelChecker.java | 58 +- prism/src/simulator/SimulatorEngine.java | 111 +- prism/src/simulator/simpctl.cc | 12 +- prism/src/simulator/simpctlbuilder.cc | 28 + 14 files changed, 2747 insertions(+), 1763 deletions(-) create mode 100644 prism/src/parser/PCTLProbBoundedFuture.java create mode 100644 prism/src/parser/PCTLProbBoundedGlobal.java create mode 100644 prism/src/parser/PCTLProbFuture.java create mode 100644 prism/src/parser/PCTLProbGlobal.java diff --git a/prism/include/SimulatorEngine.h b/prism/include/SimulatorEngine.h index 434e808c..e7143a93 100644 --- a/prism/include/SimulatorEngine.h +++ b/prism/include/SimulatorEngine.h @@ -1,981 +1,997 @@ /* DO NOT EDIT THIS FILE - it is machine generated */ -#include +#include /* Header for class simulator_SimulatorEngine */ #ifndef _Included_simulator_SimulatorEngine -#define _Included_simulator_SimulatorEngine +#define _Included_simulator_SimulatorEngine #ifdef __cplusplus extern "C" { -#endif +#endif #undef simulator_SimulatorEngine_ERROR -#define simulator_SimulatorEngine_ERROR -1L +#define simulator_SimulatorEngine_ERROR -1L #undef simulator_SimulatorEngine_OUTOFRANGE -#define simulator_SimulatorEngine_OUTOFRANGE -1L +#define simulator_SimulatorEngine_OUTOFRANGE -1L #undef simulator_SimulatorEngine_NULL -#define simulator_SimulatorEngine_NULL 0L +#define simulator_SimulatorEngine_NULL 0L #undef simulator_SimulatorEngine_NOT_LOADED -#define simulator_SimulatorEngine_NOT_LOADED 0L +#define simulator_SimulatorEngine_NOT_LOADED 0L #undef simulator_SimulatorEngine_PROBABILISTIC -#define simulator_SimulatorEngine_PROBABILISTIC 1L +#define simulator_SimulatorEngine_PROBABILISTIC 1L #undef simulator_SimulatorEngine_NONDETERMINISTIC -#define simulator_SimulatorEngine_NONDETERMINISTIC 2L +#define simulator_SimulatorEngine_NONDETERMINISTIC 2L #undef simulator_SimulatorEngine_STOCHASTIC -#define simulator_SimulatorEngine_STOCHASTIC 3L +#define simulator_SimulatorEngine_STOCHASTIC 3L #undef simulator_SimulatorEngine_UNDEFINED_INT -#define simulator_SimulatorEngine_UNDEFINED_INT -2147483647L +#define simulator_SimulatorEngine_UNDEFINED_INT -2147483647L #undef simulator_SimulatorEngine_UNDEFINED_DOUBLE -#define simulator_SimulatorEngine_UNDEFINED_DOUBLE -1.0000000138484279E24 +#define simulator_SimulatorEngine_UNDEFINED_DOUBLE -1.0000000138484279E24 #undef simulator_SimulatorEngine_INFINITY -#define simulator_SimulatorEngine_INFINITY 1.0000000138484279E24 +#define simulator_SimulatorEngine_INFINITY 1.0000000138484279E24 #undef simulator_SimulatorEngine_INTEGER -#define simulator_SimulatorEngine_INTEGER 1L +#define simulator_SimulatorEngine_INTEGER 1L #undef simulator_SimulatorEngine_DOUBLE -#define simulator_SimulatorEngine_DOUBLE 2L +#define simulator_SimulatorEngine_DOUBLE 2L #undef simulator_SimulatorEngine_BOOLEAN -#define simulator_SimulatorEngine_BOOLEAN 3L +#define simulator_SimulatorEngine_BOOLEAN 3L #undef simulator_SimulatorEngine_SIM_PATH_NUM_STEPS -#define simulator_SimulatorEngine_SIM_PATH_NUM_STEPS 0L +#define simulator_SimulatorEngine_SIM_PATH_NUM_STEPS 0L #undef simulator_SimulatorEngine_SIM_PATH_TIME -#define simulator_SimulatorEngine_SIM_PATH_TIME 1L +#define simulator_SimulatorEngine_SIM_PATH_TIME 1L #undef simulator_SimulatorEngine_SIM_PATH_DEADLOCK -#define simulator_SimulatorEngine_SIM_PATH_DEADLOCK 2L -/* - * Class: simulator_SimulatorEngine - * Method: Set_Main_Log - * Signature: (Lprism/PrismLog;)V - */ -JNIEXPORT void JNICALL Java_simulator_SimulatorEngine_Set_1Main_1Log +#define simulator_SimulatorEngine_SIM_PATH_DEADLOCK 2L +/* + * Class: simulator_SimulatorEngine + * Method: Set_Main_Log + * Signature: (Lprism/PrismLog;)V + */ +JNIEXPORT void JNICALL Java_simulator_SimulatorEngine_Set_1Main_1Log (JNIEnv *, jclass, jobject); - -/* - * Class: simulator_SimulatorEngine - * Method: tidyUpEverything - * Signature: ()I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_tidyUpEverything + +/* + * Class: simulator_SimulatorEngine + * Method: tidyUpEverything + * Signature: ()I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_tidyUpEverything (JNIEnv *, jclass); - -/* - * Class: simulator_SimulatorEngine - * Method: allocateStateSpace - * Signature: (I)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_allocateStateSpace - (JNIEnv *, jclass, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: allocateModel - * Signature: (III[I[III)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_allocateModel + +/* + * Class: simulator_SimulatorEngine + * Method: allocateStateSpace + * Signature: (I)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_allocateStateSpace + (JNIEnv *, jclass, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: allocateModel + * Signature: (III[I[III)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_allocateModel (JNIEnv *, jclass, jint, jint, jint, jintArray, jintArray, jint, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: setupAddTransition - * Signature: (I)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_setupAddTransition - (JNIEnv *, jclass, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: setupAddStateReward - * Signature: (II)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_setupAddStateReward - (JNIEnv *, jclass, jint, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: setupAddTransitionReward - * Signature: (II)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_setupAddTransitionReward - (JNIEnv *, jclass, jint, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: allocatePath - * Signature: ()I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_allocatePath + +/* + * Class: simulator_SimulatorEngine + * Method: setupAddTransition + * Signature: (I)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_setupAddTransition + (JNIEnv *, jclass, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: setupAddStateReward + * Signature: (II)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_setupAddStateReward + (JNIEnv *, jclass, jint, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: setupAddTransitionReward + * Signature: (II)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_setupAddTransitionReward + (JNIEnv *, jclass, jint, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: allocatePath + * Signature: ()I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_allocatePath (JNIEnv *, jclass); - -/* - * Class: simulator_SimulatorEngine - * Method: defineVariable - * Signature: (II)V - */ -JNIEXPORT void JNICALL Java_simulator_SimulatorEngine_defineVariable - (JNIEnv *, jclass, jint, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: startPath - * Signature: ()I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_startPath + +/* + * Class: simulator_SimulatorEngine + * Method: defineVariable + * Signature: (II)V + */ +JNIEXPORT void JNICALL Java_simulator_SimulatorEngine_defineVariable + (JNIEnv *, jclass, jint, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: startPath + * Signature: ()I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_startPath (JNIEnv *, jclass); - -/* - * Class: simulator_SimulatorEngine - * Method: getPathSize - * Signature: ()I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_getPathSize + +/* + * Class: simulator_SimulatorEngine + * Method: getPathSize + * Signature: ()I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_getPathSize (JNIEnv *, jclass); - -/* - * Class: simulator_SimulatorEngine - * Method: getPathData - * Signature: (II)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_getPathData - (JNIEnv *, jclass, jint, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: getTimeSpentInPathState - * Signature: (I)D - */ -JNIEXPORT jdouble JNICALL Java_simulator_SimulatorEngine_getTimeSpentInPathState - (JNIEnv *, jclass, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: getStateRewardOfPathState - * Signature: (II)D - */ -JNIEXPORT jdouble JNICALL Java_simulator_SimulatorEngine_getStateRewardOfPathState - (JNIEnv *, jclass, jint, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: getTransitionRewardOfPathState - * Signature: (II)D - */ -JNIEXPORT jdouble JNICALL Java_simulator_SimulatorEngine_getTransitionRewardOfPathState - (JNIEnv *, jclass, jint, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: getTotalStateRewardOfPathState - * Signature: (II)D - */ -JNIEXPORT jdouble JNICALL Java_simulator_SimulatorEngine_getTotalStateRewardOfPathState - (JNIEnv *, jclass, jint, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: getTotalTransitionRewardOfPathState - * Signature: (II)D - */ -JNIEXPORT jdouble JNICALL Java_simulator_SimulatorEngine_getTotalTransitionRewardOfPathState - (JNIEnv *, jclass, jint, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: getTotalPathTime - * Signature: ()D - */ -JNIEXPORT jdouble JNICALL Java_simulator_SimulatorEngine_getTotalPathTime + +/* + * Class: simulator_SimulatorEngine + * Method: getPathData + * Signature: (II)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_getPathData + (JNIEnv *, jclass, jint, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: getTimeSpentInPathState + * Signature: (I)D + */ +JNIEXPORT jdouble JNICALL Java_simulator_SimulatorEngine_getTimeSpentInPathState + (JNIEnv *, jclass, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: getStateRewardOfPathState + * Signature: (II)D + */ +JNIEXPORT jdouble JNICALL Java_simulator_SimulatorEngine_getStateRewardOfPathState + (JNIEnv *, jclass, jint, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: getTransitionRewardOfPathState + * Signature: (II)D + */ +JNIEXPORT jdouble JNICALL Java_simulator_SimulatorEngine_getTransitionRewardOfPathState + (JNIEnv *, jclass, jint, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: getTotalStateRewardOfPathState + * Signature: (II)D + */ +JNIEXPORT jdouble JNICALL Java_simulator_SimulatorEngine_getTotalStateRewardOfPathState + (JNIEnv *, jclass, jint, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: getTotalTransitionRewardOfPathState + * Signature: (II)D + */ +JNIEXPORT jdouble JNICALL Java_simulator_SimulatorEngine_getTotalTransitionRewardOfPathState + (JNIEnv *, jclass, jint, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: getTotalPathTime + * Signature: ()D + */ +JNIEXPORT jdouble JNICALL Java_simulator_SimulatorEngine_getTotalPathTime (JNIEnv *, jclass); - -/* - * Class: simulator_SimulatorEngine - * Method: getTotalPathReward - * Signature: (I)D - */ -JNIEXPORT jdouble JNICALL Java_simulator_SimulatorEngine_getTotalPathReward - (JNIEnv *, jclass, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: getTotalStateReward - * Signature: (I)D - */ -JNIEXPORT jdouble JNICALL Java_simulator_SimulatorEngine_getTotalStateReward - (JNIEnv *, jclass, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: getTotalTransitionReward - * Signature: (I)D - */ -JNIEXPORT jdouble JNICALL Java_simulator_SimulatorEngine_getTotalTransitionReward - (JNIEnv *, jclass, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: isPathLooping - * Signature: ()Z - */ -JNIEXPORT jboolean JNICALL Java_simulator_SimulatorEngine_isPathLooping + +/* + * Class: simulator_SimulatorEngine + * Method: getTotalPathReward + * Signature: (I)D + */ +JNIEXPORT jdouble JNICALL Java_simulator_SimulatorEngine_getTotalPathReward + (JNIEnv *, jclass, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: getTotalStateReward + * Signature: (I)D + */ +JNIEXPORT jdouble JNICALL Java_simulator_SimulatorEngine_getTotalStateReward + (JNIEnv *, jclass, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: getTotalTransitionReward + * Signature: (I)D + */ +JNIEXPORT jdouble JNICALL Java_simulator_SimulatorEngine_getTotalTransitionReward + (JNIEnv *, jclass, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: isPathLooping + * Signature: ()Z + */ +JNIEXPORT jboolean JNICALL Java_simulator_SimulatorEngine_isPathLooping (JNIEnv *, jclass); - -/* - * Class: simulator_SimulatorEngine - * Method: loopStart - * Signature: ()I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_loopStart + +/* + * Class: simulator_SimulatorEngine + * Method: loopStart + * Signature: ()I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_loopStart (JNIEnv *, jclass); - -/* - * Class: simulator_SimulatorEngine - * Method: loopEnd - * Signature: ()I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_loopEnd + +/* + * Class: simulator_SimulatorEngine + * Method: loopEnd + * Signature: ()I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_loopEnd (JNIEnv *, jclass); - -/* - * Class: simulator_SimulatorEngine - * Method: getChosenIndexOfOldUpdate - * Signature: (I)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_getChosenIndexOfOldUpdate - (JNIEnv *, jclass, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: makeManualUpdate - * Signature: (I)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_makeManualUpdate__I - (JNIEnv *, jclass, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: makeManualUpdate - * Signature: (ID)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_makeManualUpdate__ID + +/* + * Class: simulator_SimulatorEngine + * Method: getChosenIndexOfOldUpdate + * Signature: (I)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_getChosenIndexOfOldUpdate + (JNIEnv *, jclass, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: makeManualUpdate + * Signature: (I)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_makeManualUpdate__I + (JNIEnv *, jclass, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: makeManualUpdate + * Signature: (ID)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_makeManualUpdate__ID (JNIEnv *, jclass, jint, jdouble); - -/* - * Class: simulator_SimulatorEngine - * Method: doAutomaticChoices - * Signature: (IZ)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_doAutomaticChoices + +/* + * Class: simulator_SimulatorEngine + * Method: doAutomaticChoices + * Signature: (IZ)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_doAutomaticChoices (JNIEnv *, jclass, jint, jboolean); - -/* - * Class: simulator_SimulatorEngine - * Method: doBacktrack - * Signature: (I)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_doBacktrack - (JNIEnv *, jclass, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: doRemovePrecedingStates - * Signature: (I)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_doRemovePrecedingStates - (JNIEnv *, jclass, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: calculateOldUpdates - * Signature: (I)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_calculateOldUpdates - (JNIEnv *, jclass, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: finishedWithOldUpdates - * Signature: ()I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_finishedWithOldUpdates + +/* + * Class: simulator_SimulatorEngine + * Method: doBacktrack + * Signature: (I)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_doBacktrack + (JNIEnv *, jclass, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: doRemovePrecedingStates + * Signature: (I)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_doRemovePrecedingStates + (JNIEnv *, jclass, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: calculateOldUpdates + * Signature: (I)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_calculateOldUpdates + (JNIEnv *, jclass, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: finishedWithOldUpdates + * Signature: ()I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_finishedWithOldUpdates (JNIEnv *, jclass); - -/* - * Class: simulator_SimulatorEngine - * Method: getNumUpdates - * Signature: ()I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_getNumUpdates + +/* + * Class: simulator_SimulatorEngine + * Method: getNumUpdates + * Signature: ()I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_getNumUpdates (JNIEnv *, jclass); - -/* - * Class: simulator_SimulatorEngine - * Method: getActionIndexOfUpdate - * Signature: (I)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_getActionIndexOfUpdate - (JNIEnv *, jclass, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: getModuleIndexOfUpdate - * Signature: (I)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_getModuleIndexOfUpdate - (JNIEnv *, jclass, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: getProbabilityOfUpdate - * Signature: (I)D - */ -JNIEXPORT jdouble JNICALL Java_simulator_SimulatorEngine_getProbabilityOfUpdate - (JNIEnv *, jclass, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: getNumAssignmentsOfUpdate - * Signature: (I)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_getNumAssignmentsOfUpdate - (JNIEnv *, jclass, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: getAssignmentVariableIndexOfUpdate - * Signature: (II)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_getAssignmentVariableIndexOfUpdate - (JNIEnv *, jclass, jint, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: getAssignmentValueOfUpdate - * Signature: (II)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_getAssignmentValueOfUpdate - (JNIEnv *, jclass, jint, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: getDistributionIndexOfUpdate - * Signature: (I)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_getDistributionIndexOfUpdate - (JNIEnv *, jclass, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: allocatePCTLManager - * Signature: ()I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_allocatePCTLManager + +/* + * Class: simulator_SimulatorEngine + * Method: getActionIndexOfUpdate + * Signature: (I)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_getActionIndexOfUpdate + (JNIEnv *, jclass, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: getModuleIndexOfUpdate + * Signature: (I)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_getModuleIndexOfUpdate + (JNIEnv *, jclass, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: getProbabilityOfUpdate + * Signature: (I)D + */ +JNIEXPORT jdouble JNICALL Java_simulator_SimulatorEngine_getProbabilityOfUpdate + (JNIEnv *, jclass, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: getNumAssignmentsOfUpdate + * Signature: (I)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_getNumAssignmentsOfUpdate + (JNIEnv *, jclass, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: getAssignmentVariableIndexOfUpdate + * Signature: (II)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_getAssignmentVariableIndexOfUpdate + (JNIEnv *, jclass, jint, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: getAssignmentValueOfUpdate + * Signature: (II)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_getAssignmentValueOfUpdate + (JNIEnv *, jclass, jint, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: getDistributionIndexOfUpdate + * Signature: (I)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_getDistributionIndexOfUpdate + (JNIEnv *, jclass, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: allocatePCTLManager + * Signature: ()I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_allocatePCTLManager (JNIEnv *, jclass); - -/* - * Class: simulator_SimulatorEngine - * Method: allocateSampling - * Signature: ()I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_allocateSampling + +/* + * Class: simulator_SimulatorEngine + * Method: allocateSampling + * Signature: ()I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_allocateSampling (JNIEnv *, jclass); - -/* - * Class: simulator_SimulatorEngine - * Method: exportBinary - * Signature: (Ljava/lang/String;)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_exportBinary + +/* + * Class: simulator_SimulatorEngine + * Method: exportBinary + * Signature: (Ljava/lang/String;)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_exportBinary (JNIEnv *, jclass, jstring); - -/* - * Class: simulator_SimulatorEngine - * Method: doSampling - * Signature: (II)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_doSampling - (JNIEnv *, jclass, jint, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: getSamplingResult - * Signature: (I)D - */ -JNIEXPORT jdouble JNICALL Java_simulator_SimulatorEngine_getSamplingResult - (JNIEnv *, jclass, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: getNumReachedMaxPath - * Signature: (I)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_getNumReachedMaxPath - (JNIEnv *, jclass, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: stopSampling - * Signature: ()V - */ -JNIEXPORT void JNICALL Java_simulator_SimulatorEngine_stopSampling + +/* + * Class: simulator_SimulatorEngine + * Method: doSampling + * Signature: (II)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_doSampling + (JNIEnv *, jclass, jint, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: getSamplingResult + * Signature: (I)D + */ +JNIEXPORT jdouble JNICALL Java_simulator_SimulatorEngine_getSamplingResult + (JNIEnv *, jclass, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: getNumReachedMaxPath + * Signature: (I)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_getNumReachedMaxPath + (JNIEnv *, jclass, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: stopSampling + * Signature: ()V + */ +JNIEXPORT void JNICALL Java_simulator_SimulatorEngine_stopSampling (JNIEnv *, jclass); - -/* - * Class: simulator_SimulatorEngine - * Method: loadProposition - * Signature: (I)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_loadProposition - (JNIEnv *, jclass, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: queryProposition - * Signature: (I)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_queryProposition__I - (JNIEnv *, jclass, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: queryProposition - * Signature: (II)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_queryProposition__II - (JNIEnv *, jclass, jint, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: queryIsInitial - * Signature: ()I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_queryIsInitial__ + +/* + * Class: simulator_SimulatorEngine + * Method: loadProposition + * Signature: (I)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_loadProposition + (JNIEnv *, jclass, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: queryProposition + * Signature: (I)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_queryProposition__I + (JNIEnv *, jclass, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: queryProposition + * Signature: (II)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_queryProposition__II + (JNIEnv *, jclass, jint, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: queryIsInitial + * Signature: ()I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_queryIsInitial__ (JNIEnv *, jclass); - -/* - * Class: simulator_SimulatorEngine - * Method: queryIsInitial - * Signature: (I)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_queryIsInitial__I - (JNIEnv *, jclass, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: queryIsDeadlock - * Signature: ()I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_queryIsDeadlock__ + +/* + * Class: simulator_SimulatorEngine + * Method: queryIsInitial + * Signature: (I)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_queryIsInitial__I + (JNIEnv *, jclass, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: queryIsDeadlock + * Signature: ()I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_queryIsDeadlock__ (JNIEnv *, jclass); - -/* - * Class: simulator_SimulatorEngine - * Method: queryIsDeadlock - * Signature: (I)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_queryIsDeadlock__I - (JNIEnv *, jclass, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: findPathFormulaIndex - * Signature: (I)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_findPathFormulaIndex - (JNIEnv *, jclass, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: queryPathFormula - * Signature: (I)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_queryPathFormula - (JNIEnv *, jclass, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: queryPathFormulaNumeric - * Signature: (I)D - */ -JNIEXPORT jdouble JNICALL Java_simulator_SimulatorEngine_queryPathFormulaNumeric - (JNIEnv *, jclass, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: createNormalConstant - * Signature: (II)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createNormalConstant - (JNIEnv *, jclass, jint, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: createRealConstant - * Signature: (I)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createRealConstant - (JNIEnv *, jclass, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: createIntegerVar - * Signature: (I)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createIntegerVar - (JNIEnv *, jclass, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: createBooleanVar - * Signature: (I)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createBooleanVar - (JNIEnv *, jclass, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: createDouble - * Signature: (D)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createDouble + +/* + * Class: simulator_SimulatorEngine + * Method: queryIsDeadlock + * Signature: (I)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_queryIsDeadlock__I + (JNIEnv *, jclass, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: findPathFormulaIndex + * Signature: (I)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_findPathFormulaIndex + (JNIEnv *, jclass, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: queryPathFormula + * Signature: (I)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_queryPathFormula + (JNIEnv *, jclass, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: queryPathFormulaNumeric + * Signature: (I)D + */ +JNIEXPORT jdouble JNICALL Java_simulator_SimulatorEngine_queryPathFormulaNumeric + (JNIEnv *, jclass, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: createNormalConstant + * Signature: (II)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createNormalConstant + (JNIEnv *, jclass, jint, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: createRealConstant + * Signature: (I)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createRealConstant + (JNIEnv *, jclass, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: createIntegerVar + * Signature: (I)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createIntegerVar + (JNIEnv *, jclass, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: createBooleanVar + * Signature: (I)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createBooleanVar + (JNIEnv *, jclass, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: createDouble + * Signature: (D)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createDouble (JNIEnv *, jclass, jdouble); - -/* - * Class: simulator_SimulatorEngine - * Method: createInteger - * Signature: (I)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createInteger - (JNIEnv *, jclass, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: createBoolean - * Signature: (Z)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createBoolean + +/* + * Class: simulator_SimulatorEngine + * Method: createInteger + * Signature: (I)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createInteger + (JNIEnv *, jclass, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: createBoolean + * Signature: (Z)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createBoolean (JNIEnv *, jclass, jboolean); - -/* - * Class: simulator_SimulatorEngine - * Method: createCeil - * Signature: (I)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createCeil - (JNIEnv *, jclass, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: createFloor - * Signature: (I)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createFloor - (JNIEnv *, jclass, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: createNormalPow - * Signature: (II)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createNormalPow - (JNIEnv *, jclass, jint, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: createRealPow - * Signature: (II)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createRealPow - (JNIEnv *, jclass, jint, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: createMod - * Signature: (II)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createMod - (JNIEnv *, jclass, jint, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: createNot - * Signature: (I)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createNot - (JNIEnv *, jclass, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: createAnd - * Signature: ([I)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createAnd + +/* + * Class: simulator_SimulatorEngine + * Method: createCeil + * Signature: (I)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createCeil + (JNIEnv *, jclass, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: createFloor + * Signature: (I)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createFloor + (JNIEnv *, jclass, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: createNormalPow + * Signature: (II)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createNormalPow + (JNIEnv *, jclass, jint, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: createRealPow + * Signature: (II)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createRealPow + (JNIEnv *, jclass, jint, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: createMod + * Signature: (II)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createMod + (JNIEnv *, jclass, jint, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: createNot + * Signature: (I)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createNot + (JNIEnv *, jclass, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: createAnd + * Signature: ([I)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createAnd (JNIEnv *, jclass, jintArray); - -/* - * Class: simulator_SimulatorEngine - * Method: createOr - * Signature: ([I)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createOr + +/* + * Class: simulator_SimulatorEngine + * Method: createOr + * Signature: ([I)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createOr (JNIEnv *, jclass, jintArray); - -/* - * Class: simulator_SimulatorEngine - * Method: createNormalMax - * Signature: ([I)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createNormalMax + +/* + * Class: simulator_SimulatorEngine + * Method: createNormalMax + * Signature: ([I)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createNormalMax (JNIEnv *, jclass, jintArray); - -/* - * Class: simulator_SimulatorEngine - * Method: createNormalMin - * Signature: ([I)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createNormalMin + +/* + * Class: simulator_SimulatorEngine + * Method: createNormalMin + * Signature: ([I)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createNormalMin (JNIEnv *, jclass, jintArray); - -/* - * Class: simulator_SimulatorEngine - * Method: createRealMax - * Signature: ([I)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createRealMax + +/* + * Class: simulator_SimulatorEngine + * Method: createRealMax + * Signature: ([I)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createRealMax (JNIEnv *, jclass, jintArray); - -/* - * Class: simulator_SimulatorEngine - * Method: createRealMin - * Signature: ([I)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createRealMin + +/* + * Class: simulator_SimulatorEngine + * Method: createRealMin + * Signature: ([I)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createRealMin (JNIEnv *, jclass, jintArray); - -/* - * Class: simulator_SimulatorEngine - * Method: createNormalTimes - * Signature: (II)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createNormalTimes - (JNIEnv *, jclass, jint, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: createNormalPlus - * Signature: (II)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createNormalPlus - (JNIEnv *, jclass, jint, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: createNormalMinus - * Signature: (II)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createNormalMinus - (JNIEnv *, jclass, jint, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: createRealTimes - * Signature: (II)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createRealTimes - (JNIEnv *, jclass, jint, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: createRealPlus - * Signature: (II)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createRealPlus - (JNIEnv *, jclass, jint, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: createRealMinus - * Signature: (II)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createRealMinus - (JNIEnv *, jclass, jint, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: createDivide - * Signature: (II)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createDivide - (JNIEnv *, jclass, jint, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: createIte - * Signature: (III)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createIte + +/* + * Class: simulator_SimulatorEngine + * Method: createNormalTimes + * Signature: (II)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createNormalTimes + (JNIEnv *, jclass, jint, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: createNormalPlus + * Signature: (II)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createNormalPlus + (JNIEnv *, jclass, jint, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: createNormalMinus + * Signature: (II)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createNormalMinus + (JNIEnv *, jclass, jint, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: createRealTimes + * Signature: (II)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createRealTimes + (JNIEnv *, jclass, jint, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: createRealPlus + * Signature: (II)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createRealPlus + (JNIEnv *, jclass, jint, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: createRealMinus + * Signature: (II)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createRealMinus + (JNIEnv *, jclass, jint, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: createDivide + * Signature: (II)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createDivide + (JNIEnv *, jclass, jint, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: createIte + * Signature: (III)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createIte (JNIEnv *, jclass, jint, jint, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: createRealIte - * Signature: (III)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createRealIte + +/* + * Class: simulator_SimulatorEngine + * Method: createRealIte + * Signature: (III)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createRealIte (JNIEnv *, jclass, jint, jint, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: createNormalEquals - * Signature: (II)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createNormalEquals - (JNIEnv *, jclass, jint, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: createRealEquals - * Signature: (II)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createRealEquals - (JNIEnv *, jclass, jint, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: createNormalNotEquals - * Signature: (II)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createNormalNotEquals - (JNIEnv *, jclass, jint, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: createRealNotEquals - * Signature: (II)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createRealNotEquals - (JNIEnv *, jclass, jint, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: createNormalLessThan - * Signature: (II)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createNormalLessThan - (JNIEnv *, jclass, jint, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: createRealLessThan - * Signature: (II)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createRealLessThan - (JNIEnv *, jclass, jint, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: createNormalGreaterThan - * Signature: (II)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createNormalGreaterThan - (JNIEnv *, jclass, jint, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: createRealGreaterThan - * Signature: (II)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createRealGreaterThan - (JNIEnv *, jclass, jint, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: createNormalLessThanEqual - * Signature: (II)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createNormalLessThanEqual - (JNIEnv *, jclass, jint, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: createRealLessThanEqual - * Signature: (II)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createRealLessThanEqual - (JNIEnv *, jclass, jint, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: createNormalGreaterThanEqual - * Signature: (II)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createNormalGreaterThanEqual - (JNIEnv *, jclass, jint, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: createRealGreaterThanEqual - * Signature: (II)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createRealGreaterThanEqual - (JNIEnv *, jclass, jint, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: loadPctlBoundedUntil - * Signature: (IIDD)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_loadPctlBoundedUntil + +/* + * Class: simulator_SimulatorEngine + * Method: createNormalEquals + * Signature: (II)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createNormalEquals + (JNIEnv *, jclass, jint, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: createRealEquals + * Signature: (II)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createRealEquals + (JNIEnv *, jclass, jint, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: createNormalNotEquals + * Signature: (II)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createNormalNotEquals + (JNIEnv *, jclass, jint, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: createRealNotEquals + * Signature: (II)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createRealNotEquals + (JNIEnv *, jclass, jint, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: createNormalLessThan + * Signature: (II)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createNormalLessThan + (JNIEnv *, jclass, jint, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: createRealLessThan + * Signature: (II)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createRealLessThan + (JNIEnv *, jclass, jint, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: createNormalGreaterThan + * Signature: (II)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createNormalGreaterThan + (JNIEnv *, jclass, jint, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: createRealGreaterThan + * Signature: (II)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createRealGreaterThan + (JNIEnv *, jclass, jint, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: createNormalLessThanEqual + * Signature: (II)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createNormalLessThanEqual + (JNIEnv *, jclass, jint, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: createRealLessThanEqual + * Signature: (II)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createRealLessThanEqual + (JNIEnv *, jclass, jint, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: createNormalGreaterThanEqual + * Signature: (II)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createNormalGreaterThanEqual + (JNIEnv *, jclass, jint, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: createRealGreaterThanEqual + * Signature: (II)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createRealGreaterThanEqual + (JNIEnv *, jclass, jint, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: loadPctlBoundedUntil + * Signature: (IIDD)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_loadPctlBoundedUntil (JNIEnv *, jclass, jint, jint, jdouble, jdouble); - -/* - * Class: simulator_SimulatorEngine - * Method: loadPctlUntil - * Signature: (II)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_loadPctlUntil - (JNIEnv *, jclass, jint, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: loadPctlNext - * Signature: (I)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_loadPctlNext - (JNIEnv *, jclass, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: loadPctlReachability - * Signature: (II)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_loadPctlReachability - (JNIEnv *, jclass, jint, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: loadPctlCumulative - * Signature: (ID)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_loadPctlCumulative + +/* + * Class: simulator_SimulatorEngine + * Method: loadPctlBoundedUntilNegated + * Signature: (IIDD)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_loadPctlBoundedUntilNegated + (JNIEnv *, jclass, jint, jint, jdouble, jdouble); + +/* + * Class: simulator_SimulatorEngine + * Method: loadPctlUntil + * Signature: (II)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_loadPctlUntil + (JNIEnv *, jclass, jint, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: loadPctlUntilNegated + * Signature: (II)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_loadPctlUntilNegated + (JNIEnv *, jclass, jint, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: loadPctlNext + * Signature: (I)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_loadPctlNext + (JNIEnv *, jclass, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: loadPctlReachability + * Signature: (II)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_loadPctlReachability + (JNIEnv *, jclass, jint, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: loadPctlCumulative + * Signature: (ID)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_loadPctlCumulative (JNIEnv *, jclass, jint, jdouble); - -/* - * Class: simulator_SimulatorEngine - * Method: loadPctlInstantanious - * Signature: (ID)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_loadPctlInstantanious + +/* + * Class: simulator_SimulatorEngine + * Method: loadPctlInstantanious + * Signature: (ID)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_loadPctlInstantanious (JNIEnv *, jclass, jint, jdouble); - -/* - * Class: simulator_SimulatorEngine - * Method: loadProbQuestion - * Signature: (I)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_loadProbQuestion - (JNIEnv *, jclass, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: loadRewardQuestion - * Signature: (I)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_loadRewardQuestion - (JNIEnv *, jclass, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: createCommand - * Signature: (IIII)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createCommand + +/* + * Class: simulator_SimulatorEngine + * Method: loadProbQuestion + * Signature: (I)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_loadProbQuestion + (JNIEnv *, jclass, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: loadRewardQuestion + * Signature: (I)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_loadRewardQuestion + (JNIEnv *, jclass, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: createCommand + * Signature: (IIII)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createCommand (JNIEnv *, jclass, jint, jint, jint, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: addUpdate - * Signature: (III)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_addUpdate + +/* + * Class: simulator_SimulatorEngine + * Method: addUpdate + * Signature: (III)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_addUpdate (JNIEnv *, jclass, jint, jint, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: addAssignment - * Signature: (III)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_addAssignment + +/* + * Class: simulator_SimulatorEngine + * Method: addAssignment + * Signature: (III)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_addAssignment (JNIEnv *, jclass, jint, jint, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: createStateReward - * Signature: (II)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createStateReward - (JNIEnv *, jclass, jint, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: createTransitionReward - * Signature: (III)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createTransitionReward + +/* + * Class: simulator_SimulatorEngine + * Method: createStateReward + * Signature: (II)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createStateReward + (JNIEnv *, jclass, jint, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: createTransitionReward + * Signature: (III)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_createTransitionReward (JNIEnv *, jclass, jint, jint, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: printExpression - * Signature: (I)V - */ -JNIEXPORT void JNICALL Java_simulator_SimulatorEngine_printExpression - (JNIEnv *, jclass, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: expressionToString - * Signature: (I)Ljava/lang/String; - */ -JNIEXPORT jstring JNICALL Java_simulator_SimulatorEngine_expressionToString - (JNIEnv *, jclass, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: deleteExpression - * Signature: (I)V - */ -JNIEXPORT void JNICALL Java_simulator_SimulatorEngine_deleteExpression - (JNIEnv *, jclass, jint); - -/* - * Class: simulator_SimulatorEngine - * Method: modelToString - * Signature: ()Ljava/lang/String; - */ -JNIEXPORT jstring JNICALL Java_simulator_SimulatorEngine_modelToString + +/* + * Class: simulator_SimulatorEngine + * Method: printExpression + * Signature: (I)V + */ +JNIEXPORT void JNICALL Java_simulator_SimulatorEngine_printExpression + (JNIEnv *, jclass, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: expressionToString + * Signature: (I)Ljava/lang/String; + */ +JNIEXPORT jstring JNICALL Java_simulator_SimulatorEngine_expressionToString + (JNIEnv *, jclass, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: deleteExpression + * Signature: (I)V + */ +JNIEXPORT void JNICALL Java_simulator_SimulatorEngine_deleteExpression + (JNIEnv *, jclass, jint); + +/* + * Class: simulator_SimulatorEngine + * Method: modelToString + * Signature: ()Ljava/lang/String; + */ +JNIEXPORT jstring JNICALL Java_simulator_SimulatorEngine_modelToString (JNIEnv *, jclass); - -/* - * Class: simulator_SimulatorEngine - * Method: pathToString - * Signature: ()Ljava/lang/String; - */ -JNIEXPORT jstring JNICALL Java_simulator_SimulatorEngine_pathToString + +/* + * Class: simulator_SimulatorEngine + * Method: pathToString + * Signature: ()Ljava/lang/String; + */ +JNIEXPORT jstring JNICALL Java_simulator_SimulatorEngine_pathToString (JNIEnv *, jclass); - -/* - * Class: simulator_SimulatorEngine - * Method: printCurrentUpdates - * Signature: ()V - */ -JNIEXPORT void JNICALL Java_simulator_SimulatorEngine_printCurrentUpdates + +/* + * Class: simulator_SimulatorEngine + * Method: printCurrentUpdates + * Signature: ()V + */ +JNIEXPORT void JNICALL Java_simulator_SimulatorEngine_printCurrentUpdates (JNIEnv *, jclass); - -/* - * Class: simulator_SimulatorEngine - * Method: getLastErrorMessage - * Signature: ()Ljava/lang/String; - */ -JNIEXPORT jstring JNICALL Java_simulator_SimulatorEngine_getLastErrorMessage + +/* + * Class: simulator_SimulatorEngine + * Method: getLastErrorMessage + * Signature: ()Ljava/lang/String; + */ +JNIEXPORT jstring JNICALL Java_simulator_SimulatorEngine_getLastErrorMessage (JNIEnv *, jclass); - + #ifdef __cplusplus } -#endif -#endif +#endif +#endif diff --git a/prism/include/simpctl.h b/prism/include/simpctl.h index 1483afc9..6fc6f09e 100644 --- a/prism/include/simpctl.h +++ b/prism/include/simpctl.h @@ -80,7 +80,8 @@ const int FORMULA_INSTANTANEOUS = 5; class CPathFormula { protected: - bool answer; + bool answer; // the answer (true or false) + bool negate; // true if the actual result is the negation of "answer" public: bool answer_known; @@ -96,6 +97,11 @@ class CPathFormula { } + /* + * Set whether or not the value of this formula should be negated + */ + void Set_Negate(bool b); + /* * Access to the calculated answer for this CPathFormula object. */ diff --git a/prism/src/parser/PCTLProbBoundedFuture.java b/prism/src/parser/PCTLProbBoundedFuture.java new file mode 100644 index 00000000..1bd74c5e --- /dev/null +++ b/prism/src/parser/PCTLProbBoundedFuture.java @@ -0,0 +1,167 @@ +//============================================================================== +// +// Copyright (c) 2002-2004, Dave Parker +// +// This file is part of PRISM. +// +// PRISM is free software; you can redistribute it and/or modify +// it under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// PRISM is distributed in the hope that it will be useful, +// but WITHOUT ANY WARRANTY; without even the implied warranty of +// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +// GNU General Public License for more details. +// +// You should have received a copy of the GNU General Public License +// along with PRISM; if not, write to the Free Software Foundation, +// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA +// +//============================================================================== + +package parser; + +import java.util.Vector; + +import prism.PrismException; +import simulator.*; + +public class PCTLProbBoundedFuture extends PCTLFormulaUnary +{ + Expression lBound = null; // none if null, i.e. zero + Expression uBound = null; // none if null, i.e. infinity + + // constructor + + public PCTLProbBoundedFuture(PCTLFormula f, Expression l, Expression u) + { + super(f); + lBound = l; + uBound = u; + } + + public Expression getLowerBound() + { + return lBound; + } + + public Expression getUpperBound() + { + return uBound; + } + + // find all constants (i.e. locate idents which are constants) + + public PCTLFormula findAllConstants(ConstantList constantList) throws PrismException + { + // call superclass (binary) + super.findAllConstants(constantList); + // also do bound expressions + if (lBound != null) lBound = lBound.findAllConstants(constantList); + if (uBound != null) uBound = uBound.findAllConstants(constantList); + + return this; + } + + // find all variables (i.e. locate idents which are variables) + + public PCTLFormula findAllVars(Vector varIdents, Vector varTypes) throws PrismException + { + // call superclass (binary) + super.findAllVars(varIdents, varTypes); + // also do bound expressions + if (lBound != null) lBound = lBound.findAllVars(varIdents, varTypes); + if (uBound != null) uBound = uBound.findAllVars(varIdents, varTypes); + + return this; + } + + // type check + + public void typeCheck() throws PrismException + { + // call superclass (binary) + super.typeCheck(); + // check any time bounds are of type int/double + if (lBound != null) if (!(lBound.getType() == Expression.INT || lBound.getType() == Expression.DOUBLE)) { + throw new PrismException("Time bound \"" + lBound + "\" is the wrong type"); + } + if (uBound != null) if (!(uBound.getType() == Expression.INT || uBound.getType() == Expression.DOUBLE)) { + throw new PrismException("Time bound \"" + uBound + "\" is the wrong type"); + } + } + + // check everything is ok + + public void check() throws PrismException + { + // call superclass (binary) + super.check(); + // check any time bounds are ok and constant + if (lBound != null) { + lBound.check(); + if (!lBound.isConstant()) { + throw new PrismException("Time bound \"" + lBound + "\" is not constant"); + } + } + if (uBound != null) { + uBound.check(); + if (!uBound.isConstant()) { + throw new PrismException("Time bound \"" + uBound + "\" is not constant"); + } + } + } + + // check if formula is valid pctl + + public void checkValidPCTL() throws PrismException + { + // must have upper bound only + if (lBound != null) throw new PrismException("PCTL bounded future formulas must have bounds of the form \"<=k\""); + // and it must be an integer + if (uBound.getType() != Expression.INT) throw new PrismException("Bounds in PCTL bounded future formulas must be of type integer"); + } + + // check if formula is valid csl + + public void checkValidCSL() throws PrismException + { + // ok + } + + /** + * Convert and build simulator data structures + * Note: Although the simulator supports ProbBoundedFuture operators, they are + * only supported if they belong to a top-most Prob formulae, and so are not + * handled by a toSimulator method. Therefore, this method will only be called + * in error and hence throws an exception. + */ + public int toSimulator(SimulatorEngine sim ) throws SimulatorException + { + throw new SimulatorException("Unexpected Error when loading PCTL Formula into Simulator - BoundedFuture toSimulator should never be called"); + } + + // convert to string + + public String toString() + { + String s = ""; + + s += "F"; + if (lBound == null) { + s += "<=" + uBound; + } + else if (uBound == null) { + s += ">=" + lBound; + } + else { + s += "[" + lBound + "," + uBound + "]"; + } + s += " " + operand; + + return s; + } +} + +//------------------------------------------------------------------------------ diff --git a/prism/src/parser/PCTLProbBoundedGlobal.java b/prism/src/parser/PCTLProbBoundedGlobal.java new file mode 100644 index 00000000..80dad6ad --- /dev/null +++ b/prism/src/parser/PCTLProbBoundedGlobal.java @@ -0,0 +1,167 @@ +//============================================================================== +// +// Copyright (c) 2002-2004, Dave Parker +// +// This file is part of PRISM. +// +// PRISM is free software; you can redistribute it and/or modify +// it under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// PRISM is distributed in the hope that it will be useful, +// but WITHOUT ANY WARRANTY; without even the implied warranty of +// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +// GNU General Public License for more details. +// +// You should have received a copy of the GNU General Public License +// along with PRISM; if not, write to the Free Software Foundation, +// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA +// +//============================================================================== + +package parser; + +import java.util.Vector; + +import prism.PrismException; +import simulator.*; + +public class PCTLProbBoundedGlobal extends PCTLFormulaUnary +{ + Expression lBound = null; // none if null, i.e. zero + Expression uBound = null; // none if null, i.e. infinity + + // constructor + + public PCTLProbBoundedGlobal(PCTLFormula f, Expression l, Expression u) + { + super(f); + lBound = l; + uBound = u; + } + + public Expression getLowerBound() + { + return lBound; + } + + public Expression getUpperBound() + { + return uBound; + } + + // find all constants (i.e. locate idents which are constants) + + public PCTLFormula findAllConstants(ConstantList constantList) throws PrismException + { + // call superclass (binary) + super.findAllConstants(constantList); + // also do bound expressions + if (lBound != null) lBound = lBound.findAllConstants(constantList); + if (uBound != null) uBound = uBound.findAllConstants(constantList); + + return this; + } + + // find all variables (i.e. locate idents which are variables) + + public PCTLFormula findAllVars(Vector varIdents, Vector varTypes) throws PrismException + { + // call superclass (binary) + super.findAllVars(varIdents, varTypes); + // also do bound expressions + if (lBound != null) lBound = lBound.findAllVars(varIdents, varTypes); + if (uBound != null) uBound = uBound.findAllVars(varIdents, varTypes); + + return this; + } + + // type check + + public void typeCheck() throws PrismException + { + // call superclass (binary) + super.typeCheck(); + // check any time bounds are of type int/double + if (lBound != null) if (!(lBound.getType() == Expression.INT || lBound.getType() == Expression.DOUBLE)) { + throw new PrismException("Time bound \"" + lBound + "\" is the wrong type"); + } + if (uBound != null) if (!(uBound.getType() == Expression.INT || uBound.getType() == Expression.DOUBLE)) { + throw new PrismException("Time bound \"" + uBound + "\" is the wrong type"); + } + } + + // check everything is ok + + public void check() throws PrismException + { + // call superclass (binary) + super.check(); + // check any time bounds are ok and constant + if (lBound != null) { + lBound.check(); + if (!lBound.isConstant()) { + throw new PrismException("Time bound \"" + lBound + "\" is not constant"); + } + } + if (uBound != null) { + uBound.check(); + if (!uBound.isConstant()) { + throw new PrismException("Time bound \"" + uBound + "\" is not constant"); + } + } + } + + // check if formula is valid pctl + + public void checkValidPCTL() throws PrismException + { + // must have upper bound only + if (lBound != null) throw new PrismException("PCTL bounded global formulas must have bounds of the form \"<=k\""); + // and it must be an integer + if (uBound.getType() != Expression.INT) throw new PrismException("Bounds in PCTL bounded global formulas must be of type integer"); + } + + // check if formula is valid csl + + public void checkValidCSL() throws PrismException + { + // ok + } + + /** + * Convert and build simulator data structures + * Note: Although the simulator supports ProbBoundedGlobal operators, they are + * only supported if they belong to a top-most Prob formulae, and so are not + * handled by a toSimulator method. Therefore, this method will only be called + * in error and hence throws an exception. + */ + public int toSimulator(SimulatorEngine sim ) throws SimulatorException + { + throw new SimulatorException("Unexpected Error when loading PCTL Formula into Simulator - BoundedGlobal toSimulator should never be called"); + } + + // convert to string + + public String toString() + { + String s = ""; + + s += "G"; + if (lBound == null) { + s += "<=" + uBound; + } + else if (uBound == null) { + s += ">=" + lBound; + } + else { + s += "[" + lBound + "," + uBound + "]"; + } + s += " " + operand; + + return s; + } +} + +//------------------------------------------------------------------------------ diff --git a/prism/src/parser/PCTLProbFuture.java b/prism/src/parser/PCTLProbFuture.java new file mode 100644 index 00000000..45898c33 --- /dev/null +++ b/prism/src/parser/PCTLProbFuture.java @@ -0,0 +1,57 @@ +//============================================================================== +// +// Copyright (c) 2002-2004, Dave Parker +// +// This file is part of PRISM. +// +// PRISM is free software; you can redistribute it and/or modify +// it under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// PRISM is distributed in the hope that it will be useful, +// but WITHOUT ANY WARRANTY; without even the implied warranty of +// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +// GNU General Public License for more details. +// +// You should have received a copy of the GNU General Public License +// along with PRISM; if not, write to the Free Software Foundation, +// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA +// +//============================================================================== + +package parser; + +import java.util.Vector; + +import prism.PrismException; +import simulator.*; + +public class PCTLProbFuture extends PCTLFormulaUnary +{ + // constructor + + public PCTLProbFuture(PCTLFormula f) + { + super(f); + } + + /** + * Convert and build simulator data structures + * Note: Although the simulator supports ProbFuture operators, they are + * only supported if they belong to a top-most Prob formulae, and so are not + * handled by a toSimulator method. Therefore, this method will only be called + * in error and hence throws an exception. + */ + public int toSimulator(SimulatorEngine sim ) throws SimulatorException + { + throw new SimulatorException("Unexpected error when loading PCTL formula into simulator - Future toSimulator should never be called"); + } + + // convert to string + + public String toString() + { + return "F " + operand; + } +} diff --git a/prism/src/parser/PCTLProbGlobal.java b/prism/src/parser/PCTLProbGlobal.java new file mode 100644 index 00000000..dfde9cc5 --- /dev/null +++ b/prism/src/parser/PCTLProbGlobal.java @@ -0,0 +1,57 @@ +//============================================================================== +// +// Copyright (c) 2002-2004, Dave Parker +// +// This file is part of PRISM. +// +// PRISM is free software; you can redistribute it and/or modify +// it under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// PRISM is distributed in the hope that it will be useful, +// but WITHOUT ANY WARRANTY; without even the implied warranty of +// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +// GNU General Public License for more details. +// +// You should have received a copy of the GNU General Public License +// along with PRISM; if not, write to the Free Software Foundation, +// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA +// +//============================================================================== + +package parser; + +import java.util.Vector; + +import prism.PrismException; +import simulator.*; + +public class PCTLProbGlobal extends PCTLFormulaUnary +{ + // constructor + + public PCTLProbGlobal(PCTLFormula f) + { + super(f); + } + + /** + * Convert and build simulator data structures + * Note: Although the simulator supports ProbGlobal operators, they are + * only supported if they belong to a top-most Prob formulae, and so are not + * handled by a toSimulator method. Therefore, this method will only be called + * in error and hence throws an exception. + */ + public int toSimulator(SimulatorEngine sim ) throws SimulatorException + { + throw new SimulatorException("Unexpected error when loading PCTL formula into simulator - Global toSimulator should never be called"); + } + + // convert to string + + public String toString() + { + return "G " + operand; + } +} diff --git a/prism/src/parser/PrismParser.java b/prism/src/parser/PrismParser.java index 68127adc..0e690ca6 100644 --- a/prism/src/parser/PrismParser.java +++ b/prism/src/parser/PrismParser.java @@ -1461,7 +1461,7 @@ public class PrismParser implements PrismParserConstants { Token tf = null; // detects if a filter is included Token tfmin = null; // detects if min of filter requested Token tfmax = null; - if (jj_2_94(2147483647)) { + if (jj_2_96(2147483647)) { if (jj_2_81(2147483647)) { jj_consume_token(P); relOp = LtGt(); @@ -1504,26 +1504,30 @@ public class PrismParser implements PrismParserConstants { PCTLProbBoundedUntil(); } else if (jj_2_89(2147483647)) { PCTLProbUntil(); + } else if (jj_2_90(2147483647)) { + PCTLProbBoundedFutureGlobal(); + } else if (jj_2_91(2147483647)) { + PCTLProbFutureGlobal(); } else { jj_consume_token(-1); throw new ParseException(); } - if (jj_2_93(2147483647)) { + if (jj_2_95(2147483647)) { tf = jj_consume_token(LBRACE); PCTLFormula(); jj_consume_token(RBRACE); label_17: while (true) { - if (jj_2_90(2147483647)) { + if (jj_2_92(2147483647)) { ; } else { break label_17; } - if (jj_2_91(2147483647)) { + if (jj_2_93(2147483647)) { tfmin = jj_consume_token(LBRACE); jj_consume_token(MIN); jj_consume_token(RBRACE); - } else if (jj_2_92(2147483647)) { + } else if (jj_2_94(2147483647)) { tfmax = jj_consume_token(LBRACE); jj_consume_token(MAX); jj_consume_token(RBRACE); @@ -1557,7 +1561,7 @@ public class PrismParser implements PrismParserConstants { } // push result onto stack stack.push(pp); - } else if (jj_2_95(2147483647)) { + } else if (jj_2_97(2147483647)) { PCTLSS(); } else { jj_consume_token(-1); @@ -1584,13 +1588,13 @@ public class PrismParser implements PrismParserConstants { Token tr = null; PCTLFormula(); jj_consume_token(UNTIL); - if (jj_2_96(2147483647)) { + if (jj_2_98(2147483647)) { tle = jj_consume_token(LE); Expression(); - } else if (jj_2_97(2147483647)) { + } else if (jj_2_99(2147483647)) { tge = jj_consume_token(GE); Expression(); - } else if (jj_2_98(2147483647)) { + } else if (jj_2_100(2147483647)) { tr = jj_consume_token(LBRACKET); Expression(); jj_consume_token(COMMA); @@ -1647,16 +1651,101 @@ public class PrismParser implements PrismParserConstants { stack.push(u); } +// pctl bounded future (eventually) or global + static final public void PCTLProbBoundedFutureGlobal() throws ParseException { + Token tfuture = null; // detects if a future formula is used + Token tglobal = null; // detects if a global formula is used + Token tle = null; // detects if a <= time bound is used + Token tge = null; // detects if a >= time bound is used + Token tr = null; + if (jj_2_101(2147483647)) { + tfuture = jj_consume_token(FUTURE); + } else if (jj_2_102(2147483647)) { + tglobal = jj_consume_token(GLOB); + } else { + jj_consume_token(-1); + throw new ParseException(); + } + if (jj_2_103(2147483647)) { + tle = jj_consume_token(LE); + Expression(); + } else if (jj_2_104(2147483647)) { + tge = jj_consume_token(GE); + Expression(); + } else if (jj_2_105(2147483647)) { + tr = jj_consume_token(LBRACKET); + Expression(); + jj_consume_token(COMMA); + Expression(); + jj_consume_token(RBRACKET); + } else { + jj_consume_token(-1); + throw new ParseException(); + } + PCTLFormula(); + PCTLFormula f = null; + Expression lb, ub; + PCTLFormula u; + + // pop operand off stack + f = (PCTLFormula)stack.pop(); + // U<=ub + if (tle != null) { + ub = (Expression)stack.pop(); + if (tfuture != null) u = new PCTLProbBoundedFuture(f, null, ub); + else u = new PCTLProbBoundedGlobal(f, null, ub); + } + // U>=lb + else if (tge != null) { + lb = (Expression)stack.pop(); + if (tfuture != null) u = new PCTLProbBoundedFuture(f, lb, null); + else u = new PCTLProbBoundedGlobal(f, lb, null); + } + // U[lb,ub] + else { + ub = (Expression)stack.pop(); + lb = (Expression)stack.pop(); + if (tfuture != null) u = new PCTLProbBoundedFuture(f, lb, ub); + else u = new PCTLProbBoundedGlobal(f, lb, ub); + } + // push result onto stack + stack.push(u); + } + +// pctl future (eventually) or globally + static final public void PCTLProbFutureGlobal() throws ParseException { + Token tfuture = null; // detects if a future formula is used + Token tglobal = null; + if (jj_2_106(2147483647)) { + tfuture = jj_consume_token(FUTURE); + } else if (jj_2_107(2147483647)) { + tglobal = jj_consume_token(GLOB); + } else { + jj_consume_token(-1); + throw new ParseException(); + } + PCTLFormula(); + PCTLFormula f; + PCTLFormula u; + + // create PCTLProbFuture/PCTLProbGlobal object + f = (PCTLFormula)stack.pop(); + if (tfuture != null) u = new PCTLProbFuture(f); + else u = new PCTLProbGlobal(f); + // push result onto stack + stack.push(u); + } + // pctl steady state (actually only csl - not pctl at all) static final public void PCTLSS() throws ParseException { String relOp; Token tf = null; - if (jj_2_102(2147483647)) { - if (jj_2_99(2147483647)) { + if (jj_2_111(2147483647)) { + if (jj_2_108(2147483647)) { jj_consume_token(S); relOp = LtGt(); Expression(); - } else if (jj_2_100(2147483647)) { + } else if (jj_2_109(2147483647)) { jj_consume_token(S); jj_consume_token(EQ); jj_consume_token(QMARK); @@ -1667,7 +1756,7 @@ public class PrismParser implements PrismParserConstants { } jj_consume_token(LBRACKET); PCTLFormula(); - if (jj_2_101(2147483647)) { + if (jj_2_110(2147483647)) { tf = jj_consume_token(LBRACE); PCTLFormula(); jj_consume_token(RBRACE); @@ -1693,7 +1782,7 @@ public class PrismParser implements PrismParserConstants { } // push result onto stack stack.push(ss); - } else if (jj_2_103(2147483647)) { + } else if (jj_2_112(2147483647)) { PCTLReward(); } else { jj_consume_token(-1); @@ -1709,16 +1798,16 @@ public class PrismParser implements PrismParserConstants { Token tfmax = null; // detects if max of filter requested boolean b = false; // detects if a reward struct index (expression) is included String s = null; - if (jj_2_122(2147483647)) { - if (jj_2_111(2147483647)) { + if (jj_2_131(2147483647)) { + if (jj_2_120(2147483647)) { jj_consume_token(R); - if (jj_2_106(2147483647)) { + if (jj_2_115(2147483647)) { jj_consume_token(LBRACE); - if (jj_2_104(2147483647)) { + if (jj_2_113(2147483647)) { jj_consume_token(DQUOTE); s = Identifier(); jj_consume_token(DQUOTE); - } else if (jj_2_105(2147483647)) { + } else if (jj_2_114(2147483647)) { Expression(); b=true; } else { @@ -1729,19 +1818,19 @@ public class PrismParser implements PrismParserConstants { } else { ; } - if (jj_2_107(2147483647)) { + if (jj_2_116(2147483647)) { relOp = LtGt(); Expression(); - } else if (jj_2_108(2147483647)) { + } else if (jj_2_117(2147483647)) { jj_consume_token(EQ); jj_consume_token(QMARK); relOp="="; - } else if (jj_2_109(2147483647)) { + } else if (jj_2_118(2147483647)) { jj_consume_token(MIN); jj_consume_token(EQ); jj_consume_token(QMARK); relOp="min="; - } else if (jj_2_110(2147483647)) { + } else if (jj_2_119(2147483647)) { jj_consume_token(MAX); jj_consume_token(EQ); jj_consume_token(QMARK); @@ -1750,12 +1839,12 @@ public class PrismParser implements PrismParserConstants { jj_consume_token(-1); throw new ParseException(); } - } else if (jj_2_112(2147483647)) { + } else if (jj_2_121(2147483647)) { jj_consume_token(RMIN); jj_consume_token(EQ); jj_consume_token(QMARK); relOp="min="; - } else if (jj_2_113(2147483647)) { + } else if (jj_2_122(2147483647)) { jj_consume_token(RMAX); jj_consume_token(EQ); jj_consume_token(QMARK); @@ -1765,34 +1854,34 @@ public class PrismParser implements PrismParserConstants { throw new ParseException(); } jj_consume_token(LBRACKET); - if (jj_2_114(2147483647)) { + if (jj_2_123(2147483647)) { PCTLRewardCumul(); - } else if (jj_2_115(2147483647)) { + } else if (jj_2_124(2147483647)) { PCTLRewardInst(); - } else if (jj_2_116(2147483647)) { + } else if (jj_2_125(2147483647)) { PCTLRewardReach(); - } else if (jj_2_117(2147483647)) { + } else if (jj_2_126(2147483647)) { PCTLRewardSS(); } else { jj_consume_token(-1); throw new ParseException(); } - if (jj_2_121(2147483647)) { + if (jj_2_130(2147483647)) { tf = jj_consume_token(LBRACE); PCTLFormula(); jj_consume_token(RBRACE); label_18: while (true) { - if (jj_2_118(2147483647)) { + if (jj_2_127(2147483647)) { ; } else { break label_18; } - if (jj_2_119(2147483647)) { + if (jj_2_128(2147483647)) { tfmin = jj_consume_token(LBRACE); jj_consume_token(MIN); jj_consume_token(RBRACE); - } else if (jj_2_120(2147483647)) { + } else if (jj_2_129(2147483647)) { tfmax = jj_consume_token(LBRACE); jj_consume_token(MAX); jj_consume_token(RBRACE); @@ -1829,7 +1918,7 @@ public class PrismParser implements PrismParserConstants { } // push result onto stack stack.push(pr); - } else if (jj_2_123(2147483647)) { + } else if (jj_2_132(2147483647)) { PCTLInit(); } else { jj_consume_token(-1); @@ -1894,12 +1983,12 @@ public class PrismParser implements PrismParserConstants { // init static final public void PCTLInit() throws ParseException { - if (jj_2_124(2147483647)) { + if (jj_2_133(2147483647)) { jj_consume_token(DQUOTE); jj_consume_token(INIT); jj_consume_token(DQUOTE); stack.push(new PCTLInit()); - } else if (jj_2_125(2147483647)) { + } else if (jj_2_134(2147483647)) { PCTLLabel(); } else { jj_consume_token(-1); @@ -1910,12 +1999,12 @@ public class PrismParser implements PrismParserConstants { // label static final public void PCTLLabel() throws ParseException { String s; - if (jj_2_126(2147483647)) { + if (jj_2_135(2147483647)) { jj_consume_token(DQUOTE); s = Identifier(); jj_consume_token(DQUOTE); stack.push(new PCTLLabel(s)); - } else if (jj_2_127(2147483647)) { + } else if (jj_2_136(2147483647)) { PCTLBrackets(); } else { jj_consume_token(-1); @@ -1925,14 +2014,14 @@ public class PrismParser implements PrismParserConstants { // brackets static final public void PCTLBrackets() throws ParseException { - if (jj_2_128(2147483647)) { + if (jj_2_137(2147483647)) { jj_consume_token(LPARENTH); PCTLFormula(); jj_consume_token(RPARENTH); PCTLBrackets e = new PCTLBrackets(); e.setOperand((PCTLFormula)stack.pop()); stack.push(e); - } else if (jj_2_129(2147483647)) { + } else if (jj_2_138(2147483647)) { PCTLExpression(); } else { jj_consume_token(-1); @@ -1960,7 +2049,7 @@ public class PrismParser implements PrismParserConstants { Expression(); jj_consume_token(COLON); Expression(); - if (jj_2_130(2147483647)) { + if (jj_2_139(2147483647)) { t = jj_consume_token(COLON); Expression(); } else { @@ -1993,7 +2082,7 @@ public class PrismParser implements PrismParserConstants { // expression (if-then-else) static final public void ExpressionITE() throws ParseException { - if (jj_2_131(2147483647)) { + if (jj_2_140(2147483647)) { ExpressionOr(); jj_consume_token(QMARK); ExpressionOr(); @@ -2004,7 +2093,7 @@ public class PrismParser implements PrismParserConstants { t = (Expression)stack.pop(); c = (Expression)stack.pop(); stack.push(new ExpressionITE(c, t, e)); - } else if (jj_2_132(2147483647)) { + } else if (jj_2_141(2147483647)) { ExpressionOr(); } else { jj_consume_token(-1); @@ -2017,7 +2106,7 @@ public class PrismParser implements PrismParserConstants { // put '*' marker on stack stack.push(new Character('*')); ExpressionAnd(); - if (jj_2_133(2147483647)) { + if (jj_2_142(2147483647)) { jj_consume_token(OR); ExpressionOr(); } else { @@ -2051,7 +2140,7 @@ public class PrismParser implements PrismParserConstants { ExpressionNot(); label_19: while (true) { - if (jj_2_134(2147483647)) { + if (jj_2_143(2147483647)) { ; } else { break label_19; @@ -2083,7 +2172,7 @@ public class PrismParser implements PrismParserConstants { // expression (not) static final public void ExpressionNot() throws ParseException { Token t = null; - if (jj_2_135(2147483647)) { + if (jj_2_144(2147483647)) { t = jj_consume_token(NOT); } else { ; @@ -2105,7 +2194,7 @@ public class PrismParser implements PrismParserConstants { Expression e, e1, e2; // put '*' marker on stack stack.push(new Character('*')); - if (jj_2_139(2147483647)) { + if (jj_2_148(2147483647)) { ExpressionPlusMinus(); relOp = LtGt(); ExpressionPlusMinus(); @@ -2118,14 +2207,14 @@ public class PrismParser implements PrismParserConstants { stack.pop(); // push the ExpressionRelOp on to the stack stack.push(ero); - } else if (jj_2_140(2147483647)) { + } else if (jj_2_149(2147483647)) { ExpressionPlusMinus(); relOp = EqNeq(); // store the left hand side expression so that it // doesn't get mixed up with those on the right hand side e = (Expression)stack.pop(); ExpressionPlusMinus(); - if (jj_2_136(2147483647)) { + if (jj_2_145(2147483647)) { jj_consume_token(DOTS); // push a "2" on to the stack to indicate there are a pair of expressions here // (it is sandwiched between pair in stack) @@ -2136,14 +2225,14 @@ public class PrismParser implements PrismParserConstants { } label_20: while (true) { - if (jj_2_137(2147483647)) { + if (jj_2_146(2147483647)) { ; } else { break label_20; } jj_consume_token(COMMA); ExpressionPlusMinus(); - if (jj_2_138(2147483647)) { + if (jj_2_147(2147483647)) { jj_consume_token(DOTS); // push a "2" on to the stack to indicate there are a pair of expressions here // (it is sandwiched between pair in stack) @@ -2202,7 +2291,7 @@ public class PrismParser implements PrismParserConstants { // push the ExpressionRange on to the stack stack.push(er); } - } else if (jj_2_141(2147483647)) { + } else if (jj_2_150(2147483647)) { ExpressionPlusMinus(); // but still pop marker off stack e = (Expression)stack.pop(); @@ -2220,14 +2309,14 @@ public class PrismParser implements PrismParserConstants { ExpressionTimesDivide(); label_21: while (true) { - if (jj_2_142(2147483647)) { + if (jj_2_151(2147483647)) { ; } else { break label_21; } - if (jj_2_143(2147483647)) { + if (jj_2_152(2147483647)) { t = jj_consume_token(PLUS); - } else if (jj_2_144(2147483647)) { + } else if (jj_2_153(2147483647)) { t = jj_consume_token(MINUS); } else { jj_consume_token(-1); @@ -2260,14 +2349,14 @@ public class PrismParser implements PrismParserConstants { ExpressionUnaryMinus(); label_22: while (true) { - if (jj_2_145(2147483647)) { + if (jj_2_154(2147483647)) { ; } else { break label_22; } - if (jj_2_146(2147483647)) { + if (jj_2_155(2147483647)) { t = jj_consume_token(TIMES); - } else if (jj_2_147(2147483647)) { + } else if (jj_2_156(2147483647)) { t = jj_consume_token(DIVIDE); } else { jj_consume_token(-1); @@ -2296,14 +2385,14 @@ public class PrismParser implements PrismParserConstants { // expression: unary minus (right associative) static final public void ExpressionUnaryMinus() throws ParseException { - if (jj_2_148(2147483647)) { + if (jj_2_157(2147483647)) { jj_consume_token(MINUS); ExpressionFunc(); // create new expression and push to stack ExpressionUnaryMinus e = new ExpressionUnaryMinus(); e.setOperand((Expression)stack.pop()); stack.push(e); - } else if (jj_2_149(2147483647)) { + } else if (jj_2_158(2147483647)) { ExpressionFunc(); } else { jj_consume_token(-1); @@ -2317,18 +2406,18 @@ public class PrismParser implements PrismParserConstants { String s = null; // put '*' marker on stack stack.push(new Character('*')); - if (jj_2_162(2147483647)) { - if (jj_2_159(2147483647)) { - if (jj_2_150(2147483647)) { + if (jj_2_171(2147483647)) { + if (jj_2_168(2147483647)) { + if (jj_2_159(2147483647)) { jj_consume_token(MIN); s="min"; - } else if (jj_2_151(2147483647)) { + } else if (jj_2_160(2147483647)) { jj_consume_token(MAX); s="max"; - } else if (jj_2_152(2147483647)) { + } else if (jj_2_161(2147483647)) { jj_consume_token(FLOOR); s="floor"; - } else if (jj_2_153(2147483647)) { + } else if (jj_2_162(2147483647)) { jj_consume_token(CEIL); s="ceil"; } else { @@ -2336,21 +2425,21 @@ public class PrismParser implements PrismParserConstants { throw new ParseException(); } jj_consume_token(LPARENTH); - } else if (jj_2_160(2147483647)) { + } else if (jj_2_169(2147483647)) { tFunc = jj_consume_token(FUNC); jj_consume_token(LPARENTH); - if (jj_2_154(2147483647)) { + if (jj_2_163(2147483647)) { s = Identifier(); - } else if (jj_2_155(2147483647)) { + } else if (jj_2_164(2147483647)) { jj_consume_token(MIN); s="min"; - } else if (jj_2_156(2147483647)) { + } else if (jj_2_165(2147483647)) { jj_consume_token(MAX); s="max"; - } else if (jj_2_157(2147483647)) { + } else if (jj_2_166(2147483647)) { jj_consume_token(FLOOR); s="floor"; - } else if (jj_2_158(2147483647)) { + } else if (jj_2_167(2147483647)) { jj_consume_token(CEIL); s="ceil"; } else { @@ -2365,7 +2454,7 @@ public class PrismParser implements PrismParserConstants { Expression(); label_23: while (true) { - if (jj_2_161(2147483647)) { + if (jj_2_170(2147483647)) { ; } else { break label_23; @@ -2391,7 +2480,7 @@ public class PrismParser implements PrismParserConstants { e.setOldStyle(tFunc == null); // put the ExpressionFunc on the stack stack.push(e); - } else if (jj_2_163(2147483647)) { + } else if (jj_2_172(2147483647)) { ExpressionIdent(); // remove '*' marker Expression e = (Expression)stack.pop(); @@ -2406,12 +2495,12 @@ public class PrismParser implements PrismParserConstants { // expression (identifier) static final public void ExpressionIdent() throws ParseException { String ident; - if (jj_2_164(2147483647)) { + if (jj_2_173(2147483647)) { ident = Identifier(); ExpressionIdent e = new ExpressionIdent(); e.setName(ident); stack.push(e); - } else if (jj_2_165(2147483647)) { + } else if (jj_2_174(2147483647)) { ExpressionLiteral(); } else { jj_consume_token(-1); @@ -2423,25 +2512,25 @@ public class PrismParser implements PrismParserConstants { static final public void ExpressionLiteral() throws ParseException { int i; String d; - if (jj_2_166(2147483647)) { + if (jj_2_175(2147483647)) { i = Int(); ExpressionInt e = new ExpressionInt(); e.setValue(i); stack.push(e); - } else if (jj_2_167(2147483647)) { + } else if (jj_2_176(2147483647)) { d = Double(); ExpressionDouble e = new ExpressionDouble(); e.setValue(d); stack.push(e); - } else if (jj_2_168(2147483647)) { + } else if (jj_2_177(2147483647)) { jj_consume_token(TRUE); ExpressionTrue e = new ExpressionTrue(); stack.push(e); - } else if (jj_2_169(2147483647)) { + } else if (jj_2_178(2147483647)) { jj_consume_token(FALSE); ExpressionFalse e = new ExpressionFalse(); stack.push(e); - } else if (jj_2_170(2147483647)) { + } else if (jj_2_179(2147483647)) { ExpressionBrackets(); } else { jj_consume_token(-1); @@ -2482,9 +2571,9 @@ public class PrismParser implements PrismParserConstants { // one of the relational operators: =, != static final public String EqNeq() throws ParseException { - if (jj_2_171(2147483647)) { + if (jj_2_180(2147483647)) { jj_consume_token(EQ); - } else if (jj_2_172(2147483647)) { + } else if (jj_2_181(2147483647)) { jj_consume_token(NE); } else { jj_consume_token(-1); @@ -2496,13 +2585,13 @@ public class PrismParser implements PrismParserConstants { // one of the relational operators: >, <, >=, <= static final public String LtGt() throws ParseException { - if (jj_2_173(2147483647)) { + if (jj_2_182(2147483647)) { jj_consume_token(GT); - } else if (jj_2_174(2147483647)) { + } else if (jj_2_183(2147483647)) { jj_consume_token(LT); - } else if (jj_2_175(2147483647)) { + } else if (jj_2_184(2147483647)) { jj_consume_token(GE); - } else if (jj_2_176(2147483647)) { + } else if (jj_2_185(2147483647)) { jj_consume_token(LE); } else { jj_consume_token(-1); @@ -3761,43 +3850,107 @@ public class PrismParser implements PrismParserConstants { finally { jj_save(175, xla); } } - static final private boolean jj_3_34() { - if (jj_3R_38()) return true; - return false; + static final private boolean jj_2_177(int xla) { + jj_la = xla; jj_lastpos = jj_scanpos = token; + try { return !jj_3_177(); } + catch(LookaheadSuccess ls) { return true; } + finally { jj_save(176, xla); } } - static final private boolean jj_3_176() { - if (jj_scan_token(LE)) return true; + static final private boolean jj_2_178(int xla) { + jj_la = xla; jj_lastpos = jj_scanpos = token; + try { return !jj_3_178(); } + catch(LookaheadSuccess ls) { return true; } + finally { jj_save(177, xla); } + } + + static final private boolean jj_2_179(int xla) { + jj_la = xla; jj_lastpos = jj_scanpos = token; + try { return !jj_3_179(); } + catch(LookaheadSuccess ls) { return true; } + finally { jj_save(178, xla); } + } + + static final private boolean jj_2_180(int xla) { + jj_la = xla; jj_lastpos = jj_scanpos = token; + try { return !jj_3_180(); } + catch(LookaheadSuccess ls) { return true; } + finally { jj_save(179, xla); } + } + + static final private boolean jj_2_181(int xla) { + jj_la = xla; jj_lastpos = jj_scanpos = token; + try { return !jj_3_181(); } + catch(LookaheadSuccess ls) { return true; } + finally { jj_save(180, xla); } + } + + static final private boolean jj_2_182(int xla) { + jj_la = xla; jj_lastpos = jj_scanpos = token; + try { return !jj_3_182(); } + catch(LookaheadSuccess ls) { return true; } + finally { jj_save(181, xla); } + } + + static final private boolean jj_2_183(int xla) { + jj_la = xla; jj_lastpos = jj_scanpos = token; + try { return !jj_3_183(); } + catch(LookaheadSuccess ls) { return true; } + finally { jj_save(182, xla); } + } + + static final private boolean jj_2_184(int xla) { + jj_la = xla; jj_lastpos = jj_scanpos = token; + try { return !jj_3_184(); } + catch(LookaheadSuccess ls) { return true; } + finally { jj_save(183, xla); } + } + + static final private boolean jj_2_185(int xla) { + jj_la = xla; jj_lastpos = jj_scanpos = token; + try { return !jj_3_185(); } + catch(LookaheadSuccess ls) { return true; } + finally { jj_save(184, xla); } + } + + static final private boolean jj_3_34() { + if (jj_3R_38()) return true; return false; } - static final private boolean jj_3_135() { - if (jj_scan_token(NOT)) return true; + static final private boolean jj_3_139() { + if (jj_scan_token(COLON)) return true; + if (jj_3R_35()) return true; return false; } static final private boolean jj_3R_72() { + if (jj_3R_92()) return true; Token xsp; xsp = jj_scanpos; - if (jj_3_135()) jj_scanpos = xsp; - if (jj_3R_89()) return true; + if (jj_3_142()) jj_scanpos = xsp; + return false; + } + + static final private boolean jj_3_166() { + if (jj_scan_token(FLOOR)) return true; return false; } static final private boolean jj_3R_58() { - if (jj_3R_59()) return true; + if (jj_3R_61()) return true; if (jj_scan_token(UNTIL)) return true; - if (jj_3R_59()) return true; + if (jj_3R_61()) return true; return false; } - static final private boolean jj_3_175() { - if (jj_scan_token(GE)) return true; + static final private boolean jj_3_91() { + if (jj_3R_60()) return true; return false; } - static final private boolean jj_3R_80() { - if (jj_scan_token(REG_INT)) return true; + static final private boolean jj_3_141() { + if (jj_3R_72()) return true; return false; } @@ -3814,13 +3967,15 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3_174() { - if (jj_scan_token(LT)) return true; + static final private boolean jj_3R_84() { + if (jj_scan_token(LPARENTH)) return true; + if (jj_3R_35()) return true; + if (jj_scan_token(RPARENTH)) return true; return false; } static final private boolean jj_3R_47() { - if (jj_3R_86()) return true; + if (jj_3R_88()) return true; Token xsp; while (true) { xsp = jj_scanpos; @@ -3829,46 +3984,53 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3_134() { - if (jj_scan_token(AND)) return true; - if (jj_3R_72()) return true; - return false; - } - static final private boolean jj_3_33() { if (jj_3R_37()) return true; return false; } - static final private boolean jj_3_96() { + static final private boolean jj_3_98() { if (jj_scan_token(LE)) return true; if (jj_3R_35()) return true; return false; } - static final private boolean jj_3_173() { - if (jj_scan_token(GT)) return true; - return false; - } - - static final private boolean jj_3R_55() { + static final private boolean jj_3R_73() { Token xsp; xsp = jj_scanpos; - if (jj_3_173()) { - jj_scanpos = xsp; - if (jj_3_174()) { - jj_scanpos = xsp; - if (jj_3_175()) { + if (jj_3_140()) { jj_scanpos = xsp; - if (jj_3_176()) return true; - } - } + if (jj_3_141()) return true; } return false; } - static final private boolean jj_3_172() { - if (jj_scan_token(NE)) return true; + static final private boolean jj_3_179() { + if (jj_3R_84()) return true; + return false; + } + + static final private boolean jj_3_140() { + if (jj_3R_72()) return true; + if (jj_scan_token(QMARK)) return true; + if (jj_3R_72()) return true; + if (jj_scan_token(COLON)) return true; + if (jj_3R_73()) return true; + return false; + } + + static final private boolean jj_3_162() { + if (jj_scan_token(CEIL)) return true; + return false; + } + + static final private boolean jj_3_178() { + if (jj_scan_token(FALSE)) return true; + return false; + } + + static final private boolean jj_3_165() { + if (jj_scan_token(MAX)) return true; return false; } @@ -3882,33 +4044,23 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3_171() { - if (jj_scan_token(EQ)) return true; + static final private boolean jj_3R_35() { + if (jj_3R_73()) return true; return false; } - static final private boolean jj_3R_74() { - Token xsp; - xsp = jj_scanpos; - if (jj_3_171()) { - jj_scanpos = xsp; - if (jj_3_172()) return true; - } + static final private boolean jj_3_177() { + if (jj_scan_token(TRUE)) return true; return false; } - static final private boolean jj_3R_90() { - if (jj_3R_72()) return true; - Token xsp; - while (true) { - xsp = jj_scanpos; - if (jj_3_134()) { jj_scanpos = xsp; break; } - } + static final private boolean jj_3_90() { + if (jj_3R_59()) return true; return false; } - static final private boolean jj_3_158() { - if (jj_scan_token(CEIL)) return true; + static final private boolean jj_3_176() { + if (jj_3R_83()) return true; return false; } @@ -3919,18 +4071,18 @@ public class PrismParser implements PrismParserConstants { } static final private boolean jj_3R_57() { - if (jj_3R_59()) return true; + if (jj_3R_61()) return true; if (jj_scan_token(UNTIL)) return true; Token xsp; xsp = jj_scanpos; - if (jj_3_96()) { + if (jj_3_98()) { jj_scanpos = xsp; - if (jj_3_97()) { + if (jj_3_99()) { jj_scanpos = xsp; - if (jj_3_98()) return true; + if (jj_3_100()) return true; } } - if (jj_3R_59()) return true; + if (jj_3R_61()) return true; return false; } @@ -3958,9 +4110,22 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3_133() { - if (jj_scan_token(OR)) return true; - if (jj_3R_70()) return true; + static final private boolean jj_3R_81() { + Token xsp; + xsp = jj_scanpos; + if (jj_3_175()) { + jj_scanpos = xsp; + if (jj_3_176()) { + jj_scanpos = xsp; + if (jj_3_177()) { + jj_scanpos = xsp; + if (jj_3_178()) { + jj_scanpos = xsp; + if (jj_3_179()) return true; + } + } + } + } return false; } @@ -3980,8 +4145,18 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_42() { - if (jj_scan_token(REG_IDENTPRIME)) return true; + static final private boolean jj_3_175() { + if (jj_3R_82()) return true; + return false; + } + + static final private boolean jj_3_161() { + if (jj_scan_token(FLOOR)) return true; + return false; + } + + static final private boolean jj_3_164() { + if (jj_scan_token(MIN)) return true; return false; } @@ -3990,6 +4165,11 @@ public class PrismParser implements PrismParserConstants { return false; } + static final private boolean jj_3_174() { + if (jj_3R_81()) return true; + return false; + } + static final private boolean jj_3_57() { if (jj_scan_token(FLOOR)) return true; return false; @@ -4000,18 +4180,13 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3_92() { + static final private boolean jj_3_94() { if (jj_scan_token(LBRACE)) return true; if (jj_scan_token(MAX)) return true; if (jj_scan_token(RBRACE)) return true; return false; } - static final private boolean jj_3R_36() { - if (jj_scan_token(REG_IDENT)) return true; - return false; - } - static final private boolean jj_3R_27() { if (jj_scan_token(GLOBAL)) return true; if (jj_3R_37()) return true; @@ -4020,37 +4195,33 @@ public class PrismParser implements PrismParserConstants { static final private boolean jj_3R_56() { if (jj_scan_token(NEXT)) return true; - if (jj_3R_59()) return true; - return false; - } - - static final private boolean jj_3_24() { - if (jj_scan_token(EQ)) return true; - if (jj_3R_35()) return true; + if (jj_3R_61()) return true; return false; } - static final private boolean jj_3_130() { - if (jj_scan_token(COLON)) return true; - if (jj_3R_35()) return true; + static final private boolean jj_3R_80() { + Token xsp; + xsp = jj_scanpos; + if (jj_3_173()) { + jj_scanpos = xsp; + if (jj_3_174()) return true; + } return false; } - static final private boolean jj_3_26() { - if (jj_scan_token(PROB)) return true; + static final private boolean jj_3_173() { + if (jj_3R_36()) return true; return false; } - static final private boolean jj_3R_70() { - if (jj_3R_90()) return true; - Token xsp; - xsp = jj_scanpos; - if (jj_3_133()) jj_scanpos = xsp; + static final private boolean jj_3_24() { + if (jj_scan_token(EQ)) return true; + if (jj_3R_35()) return true; return false; } - static final private boolean jj_3_157() { - if (jj_scan_token(FLOOR)) return true; + static final private boolean jj_3_26() { + if (jj_scan_token(PROB)) return true; return false; } @@ -4065,8 +4236,8 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3_95() { - if (jj_3R_60()) return true; + static final private boolean jj_3_97() { + if (jj_3R_62()) return true; return false; } @@ -4083,20 +4254,28 @@ public class PrismParser implements PrismParserConstants { return false; } + static final private boolean jj_3_163() { + if (jj_3R_36()) return true; + return false; + } + static final private boolean jj_3_25() { if (jj_scan_token(RATE)) return true; return false; } - static final private boolean jj_3_132() { - if (jj_3R_70()) return true; + static final private boolean jj_3_160() { + if (jj_scan_token(MAX)) return true; return false; } - static final private boolean jj_3R_82() { - if (jj_scan_token(LPARENTH)) return true; - if (jj_3R_35()) return true; - if (jj_scan_token(RPARENTH)) return true; + static final private boolean jj_3R_71() { + if (jj_3R_91()) return true; + return false; + } + + static final private boolean jj_3_172() { + if (jj_3R_80()) return true; return false; } @@ -4125,18 +4304,9 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_71() { - Token xsp; - xsp = jj_scanpos; - if (jj_3_131()) { - jj_scanpos = xsp; - if (jj_3_132()) return true; - } - return false; - } - static final private boolean jj_3_170() { - if (jj_3R_82()) return true; + if (jj_scan_token(COMMA)) return true; + if (jj_3R_35()) return true; return false; } @@ -4145,20 +4315,6 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3_131() { - if (jj_3R_70()) return true; - if (jj_scan_token(QMARK)) return true; - if (jj_3R_70()) return true; - if (jj_scan_token(COLON)) return true; - if (jj_3R_71()) return true; - return false; - } - - static final private boolean jj_3_153() { - if (jj_scan_token(CEIL)) return true; - return false; - } - static final private boolean jj_3_51() { if (jj_scan_token(MAX)) return true; return false; @@ -4174,13 +4330,8 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3_169() { - if (jj_scan_token(FALSE)) return true; - return false; - } - - static final private boolean jj_3_156() { - if (jj_scan_token(MAX)) return true; + static final private boolean jj_3_138() { + if (jj_3R_71()) return true; return false; } @@ -4195,36 +4346,31 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_35() { - if (jj_3R_71()) return true; - return false; - } - - static final private boolean jj_3_90() { + static final private boolean jj_3_92() { Token xsp; xsp = jj_scanpos; - if (jj_3_91()) { + if (jj_3_93()) { jj_scanpos = xsp; - if (jj_3_92()) return true; + if (jj_3_94()) return true; } return false; } - static final private boolean jj_3_91() { + static final private boolean jj_3_93() { if (jj_scan_token(LBRACE)) return true; if (jj_scan_token(MIN)) return true; if (jj_scan_token(RBRACE)) return true; return false; } - static final private boolean jj_3_93() { + static final private boolean jj_3_95() { if (jj_scan_token(LBRACE)) return true; - if (jj_3R_59()) return true; + if (jj_3R_61()) return true; if (jj_scan_token(RBRACE)) return true; Token xsp; while (true) { xsp = jj_scanpos; - if (jj_3_90()) { jj_scanpos = xsp; break; } + if (jj_3_92()) { jj_scanpos = xsp; break; } } return false; } @@ -4234,17 +4380,56 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3_168() { - if (jj_scan_token(TRUE)) return true; - return false; - } - static final private boolean jj_3_21() { if (jj_scan_token(EQ)) return true; if (jj_3R_35()) return true; return false; } + static final private boolean jj_3R_70() { + Token xsp; + xsp = jj_scanpos; + if (jj_3_137()) { + jj_scanpos = xsp; + if (jj_3_138()) return true; + } + return false; + } + + static final private boolean jj_3_169() { + if (jj_scan_token(FUNC)) return true; + if (jj_scan_token(LPARENTH)) return true; + Token xsp; + xsp = jj_scanpos; + if (jj_3_163()) { + jj_scanpos = xsp; + if (jj_3_164()) { + jj_scanpos = xsp; + if (jj_3_165()) { + jj_scanpos = xsp; + if (jj_3_166()) { + jj_scanpos = xsp; + if (jj_3_167()) return true; + } + } + } + } + if (jj_scan_token(COMMA)) return true; + return false; + } + + static final private boolean jj_3_159() { + if (jj_scan_token(MIN)) return true; + return false; + } + + static final private boolean jj_3_137() { + if (jj_scan_token(LPARENTH)) return true; + if (jj_3R_61()) return true; + if (jj_scan_token(RPARENTH)) return true; + return false; + } + static final private boolean jj_3_20() { if (jj_scan_token(CTMC)) return true; return false; @@ -4257,6 +4442,23 @@ public class PrismParser implements PrismParserConstants { return false; } + static final private boolean jj_3_168() { + Token xsp; + xsp = jj_scanpos; + if (jj_3_159()) { + jj_scanpos = xsp; + if (jj_3_160()) { + jj_scanpos = xsp; + if (jj_3_161()) { + jj_scanpos = xsp; + if (jj_3_162()) return true; + } + } + } + if (jj_scan_token(LPARENTH)) return true; + return false; + } + static final private boolean jj_3_85() { if (jj_scan_token(PMIN)) return true; if (jj_scan_token(EQ)) return true; @@ -4264,6 +4466,32 @@ public class PrismParser implements PrismParserConstants { return false; } + static final private boolean jj_3R_79() { + Token xsp; + xsp = jj_scanpos; + if (jj_3_171()) { + jj_scanpos = xsp; + if (jj_3_172()) return true; + } + return false; + } + + static final private boolean jj_3_171() { + Token xsp; + xsp = jj_scanpos; + if (jj_3_168()) { + jj_scanpos = xsp; + if (jj_3_169()) return true; + } + if (jj_3R_35()) return true; + while (true) { + xsp = jj_scanpos; + if (jj_3_170()) { jj_scanpos = xsp; break; } + } + if (jj_scan_token(RPARENTH)) return true; + return false; + } + static final private boolean jj_3_84() { if (jj_scan_token(P)) return true; if (jj_scan_token(MAX)) return true; @@ -4272,11 +4500,6 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3_167() { - if (jj_3R_81()) return true; - return false; - } - static final private boolean jj_3_30() { if (jj_scan_token(CONST)) return true; if (jj_scan_token(BOOL)) return true; @@ -4315,17 +4538,22 @@ public class PrismParser implements PrismParserConstants { return false; } + static final private boolean jj_3_136() { + if (jj_3R_70()) return true; + return false; + } + static final private boolean jj_3_61() { if (jj_3R_46()) return true; return false; } - static final private boolean jj_3R_87() { + static final private boolean jj_3R_89() { Token xsp; xsp = jj_scanpos; - if (jj_3_94()) { + if (jj_3_96()) { jj_scanpos = xsp; - if (jj_3_95()) return true; + if (jj_3_97()) return true; } return false; } @@ -4335,7 +4563,7 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3_94() { + static final private boolean jj_3_96() { Token xsp; xsp = jj_scanpos; if (jj_3_81()) { @@ -4360,11 +4588,17 @@ public class PrismParser implements PrismParserConstants { jj_scanpos = xsp; if (jj_3_88()) { jj_scanpos = xsp; - if (jj_3_89()) return true; + if (jj_3_89()) { + jj_scanpos = xsp; + if (jj_3_90()) { + jj_scanpos = xsp; + if (jj_3_91()) return true; + } + } } } xsp = jj_scanpos; - if (jj_3_93()) jj_scanpos = xsp; + if (jj_3_95()) jj_scanpos = xsp; if (jj_scan_token(RBRACKET)) return true; return false; } @@ -4374,7 +4608,7 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_84() { + static final private boolean jj_3R_86() { Token xsp; xsp = jj_scanpos; if (jj_3_59()) { @@ -4390,30 +4624,6 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_79() { - Token xsp; - xsp = jj_scanpos; - if (jj_3_166()) { - jj_scanpos = xsp; - if (jj_3_167()) { - jj_scanpos = xsp; - if (jj_3_168()) { - jj_scanpos = xsp; - if (jj_3_169()) { - jj_scanpos = xsp; - if (jj_3_170()) return true; - } - } - } - } - return false; - } - - static final private boolean jj_3_166() { - if (jj_3R_80()) return true; - return false; - } - static final private boolean jj_3_59() { if (jj_3R_44()) return true; return false; @@ -4424,21 +4634,38 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3_50() { - if (jj_scan_token(MIN)) return true; - return false; - } - - static final private boolean jj_3_152() { - if (jj_scan_token(FLOOR)) return true; + static final private boolean jj_3R_69() { + Token xsp; + xsp = jj_scanpos; + if (jj_3_135()) { + jj_scanpos = xsp; + if (jj_3_136()) return true; + } return false; } - static final private boolean jj_3_155() { + static final private boolean jj_3_50() { if (jj_scan_token(MIN)) return true; return false; } + static final private boolean jj_3_135() { + if (jj_scan_token(DQUOTE)) return true; + if (jj_3R_36()) return true; + if (jj_scan_token(DQUOTE)) return true; + return false; + } + + static final private boolean jj_3_156() { + if (jj_scan_token(DIVIDE)) return true; + return false; + } + + static final private boolean jj_3_158() { + if (jj_3R_79()) return true; + return false; + } + static final private boolean jj_3_29() { if (jj_scan_token(CONST)) return true; if (jj_scan_token(DOUBLE)) return true; @@ -4455,43 +4682,77 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3_165() { - if (jj_3R_79()) return true; + static final private boolean jj_3_134() { + if (jj_3R_69()) return true; return false; } static final private boolean jj_3R_30() { if (jj_scan_token(SYSTEM)) return true; - if (jj_3R_84()) return true; + if (jj_3R_86()) return true; if (jj_scan_token(ENDSYSTEM)) return true; return false; } + static final private boolean jj_3R_78() { + Token xsp; + xsp = jj_scanpos; + if (jj_3_157()) { + jj_scanpos = xsp; + if (jj_3_158()) return true; + } + return false; + } + + static final private boolean jj_3_157() { + if (jj_scan_token(MINUS)) return true; + if (jj_3R_79()) return true; + return false; + } + + static final private boolean jj_3_155() { + if (jj_scan_token(TIMES)) return true; + return false; + } + static final private boolean jj_3_80() { if (jj_scan_token(NOT)) return true; return false; } - static final private boolean jj_3R_78() { + static final private boolean jj_3R_68() { Token xsp; xsp = jj_scanpos; - if (jj_3_164()) { + if (jj_3_133()) { jj_scanpos = xsp; - if (jj_3_165()) return true; + if (jj_3_134()) return true; } return false; } - static final private boolean jj_3R_54() { + static final private boolean jj_3_133() { + if (jj_scan_token(DQUOTE)) return true; + if (jj_scan_token(INIT)) return true; + if (jj_scan_token(DQUOTE)) return true; + return false; + } + + static final private boolean jj_3_154() { Token xsp; xsp = jj_scanpos; - if (jj_3_80()) jj_scanpos = xsp; - if (jj_3R_87()) return true; + if (jj_3_155()) { + jj_scanpos = xsp; + if (jj_3_156()) return true; + } + if (jj_3R_78()) return true; return false; } - static final private boolean jj_3_164() { - if (jj_3R_36()) return true; + static final private boolean jj_3R_54() { + Token xsp; + xsp = jj_scanpos; + if (jj_3_80()) jj_scanpos = xsp; + if (jj_3R_89()) return true; return false; } @@ -4580,23 +4841,13 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3_154() { - if (jj_3R_36()) return true; - return false; - } - - static final private boolean jj_3_151() { - if (jj_scan_token(MAX)) return true; - return false; - } - - static final private boolean jj_3R_69() { - if (jj_3R_89()) return true; + static final private boolean jj_3R_67() { + if (jj_scan_token(S)) return true; return false; } - static final private boolean jj_3_163() { - if (jj_3R_78()) return true; + static final private boolean jj_3_153() { + if (jj_scan_token(MINUS)) return true; return false; } @@ -4606,7 +4857,7 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_83() { + static final private boolean jj_3R_85() { if (jj_3R_43()) return true; Token xsp; while (true) { @@ -4627,12 +4878,6 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3_161() { - if (jj_scan_token(COMMA)) return true; - if (jj_3R_35()) return true; - return false; - } - static final private boolean jj_3_10() { if (jj_3R_32()) return true; return false; @@ -4643,88 +4888,54 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3_129() { - if (jj_3R_69()) return true; - return false; - } - - static final private boolean jj_3R_53() { - if (jj_3R_54()) return true; + static final private boolean jj_3R_77() { + if (jj_3R_78()) return true; Token xsp; while (true) { xsp = jj_scanpos; - if (jj_3_79()) { jj_scanpos = xsp; break; } + if (jj_3_154()) { jj_scanpos = xsp; break; } } return false; } - static final private boolean jj_3R_25() { - if (jj_scan_token(FORMULA)) return true; - if (jj_3R_36()) return true; - if (jj_scan_token(EQ)) return true; - if (jj_3R_35()) return true; - if (jj_scan_token(SEMICOLON)) return true; + static final private boolean jj_3_152() { + if (jj_scan_token(PLUS)) return true; return false; } - static final private boolean jj_3R_68() { + static final private boolean jj_3_151() { Token xsp; xsp = jj_scanpos; - if (jj_3_128()) { + if (jj_3_152()) { jj_scanpos = xsp; - if (jj_3_129()) return true; + if (jj_3_153()) return true; } + if (jj_3R_77()) return true; return false; } - static final private boolean jj_3_160() { - if (jj_scan_token(FUNC)) return true; - if (jj_scan_token(LPARENTH)) return true; + static final private boolean jj_3R_53() { + if (jj_3R_54()) return true; Token xsp; - xsp = jj_scanpos; - if (jj_3_154()) { - jj_scanpos = xsp; - if (jj_3_155()) { - jj_scanpos = xsp; - if (jj_3_156()) { - jj_scanpos = xsp; - if (jj_3_157()) { - jj_scanpos = xsp; - if (jj_3_158()) return true; - } - } - } + while (true) { + xsp = jj_scanpos; + if (jj_3_79()) { jj_scanpos = xsp; break; } } - if (jj_scan_token(COMMA)) return true; - return false; - } - - static final private boolean jj_3_150() { - if (jj_scan_token(MIN)) return true; return false; } - static final private boolean jj_3_128() { - if (jj_scan_token(LPARENTH)) return true; - if (jj_3R_59()) return true; - if (jj_scan_token(RPARENTH)) return true; + static final private boolean jj_3R_25() { + if (jj_scan_token(FORMULA)) return true; + if (jj_3R_36()) return true; + if (jj_scan_token(EQ)) return true; + if (jj_3R_35()) return true; + if (jj_scan_token(SEMICOLON)) return true; return false; } - static final private boolean jj_3_159() { - Token xsp; - xsp = jj_scanpos; - if (jj_3_150()) { - jj_scanpos = xsp; - if (jj_3_151()) { - jj_scanpos = xsp; - if (jj_3_152()) { - jj_scanpos = xsp; - if (jj_3_153()) return true; - } - } - } - if (jj_scan_token(LPARENTH)) return true; + static final private boolean jj_3R_66() { + if (jj_scan_token(FUTURE)) return true; + if (jj_3R_61()) return true; return false; } @@ -4733,39 +4944,13 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_77() { - Token xsp; - xsp = jj_scanpos; - if (jj_3_162()) { - jj_scanpos = xsp; - if (jj_3_163()) return true; - } - return false; - } - - static final private boolean jj_3_162() { - Token xsp; - xsp = jj_scanpos; - if (jj_3_159()) { - jj_scanpos = xsp; - if (jj_3_160()) return true; - } - if (jj_3R_35()) return true; - while (true) { - xsp = jj_scanpos; - if (jj_3_161()) { jj_scanpos = xsp; break; } - } - if (jj_scan_token(RPARENTH)) return true; - return false; - } - static final private boolean jj_3R_29() { if (jj_scan_token(MODULE)) return true; if (jj_3R_36()) return true; if (jj_scan_token(EQ)) return true; if (jj_3R_36()) return true; if (jj_scan_token(LBRACKET)) return true; - if (jj_3R_83()) return true; + if (jj_3R_85()) return true; if (jj_scan_token(RBRACKET)) return true; if (jj_scan_token(ENDMODULE)) return true; return false; @@ -4776,11 +4961,6 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3_127() { - if (jj_3R_68()) return true; - return false; - } - static final private boolean jj_3R_24() { Token xsp; xsp = jj_scanpos; @@ -4809,35 +4989,30 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_67() { - Token xsp; - xsp = jj_scanpos; - if (jj_3_126()) { - jj_scanpos = xsp; - if (jj_3_127()) return true; - } - return false; - } - static final private boolean jj_3_126() { - if (jj_scan_token(DQUOTE)) return true; - if (jj_3R_36()) return true; - if (jj_scan_token(DQUOTE)) return true; + if (jj_3R_67()) return true; return false; } - static final private boolean jj_3_147() { - if (jj_scan_token(DIVIDE)) return true; + static final private boolean jj_3R_65() { + if (jj_scan_token(INST)) return true; + if (jj_scan_token(EQ)) return true; + if (jj_3R_35()) return true; return false; } - static final private boolean jj_3_149() { - if (jj_3R_77()) return true; + static final private boolean jj_3_8() { + if (jj_3R_30()) return true; return false; } - static final private boolean jj_3_8() { - if (jj_3R_30()) return true; + static final private boolean jj_3R_75() { + if (jj_3R_77()) return true; + Token xsp; + while (true) { + xsp = jj_scanpos; + if (jj_3_151()) { jj_scanpos = xsp; break; } + } return false; } @@ -4848,11 +5023,6 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3_125() { - if (jj_3R_67()) return true; - return false; - } - static final private boolean jj_3R_52() { if (jj_3R_53()) return true; Token xsp; @@ -4863,91 +5033,71 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_76() { + static final private boolean jj_3_77() { + if (jj_scan_token(IMPLIES)) return true; + if (jj_3R_52()) return true; + return false; + } + + static final private boolean jj_3R_41() { Token xsp; xsp = jj_scanpos; - if (jj_3_148()) { + if (jj_3_46()) { jj_scanpos = xsp; - if (jj_3_149()) return true; + if (jj_3_47()) return true; } return false; } - static final private boolean jj_3_148() { - if (jj_scan_token(MINUS)) return true; - if (jj_3R_77()) return true; + static final private boolean jj_3_46() { + if (jj_scan_token(LPARENTH)) return true; + if (jj_3R_42()) return true; + if (jj_scan_token(EQ)) return true; + if (jj_3R_35()) return true; + if (jj_scan_token(RPARENTH)) return true; return false; } - static final private boolean jj_3_146() { - if (jj_scan_token(TIMES)) return true; + static final private boolean jj_3_14() { + if (jj_3R_34()) return true; return false; } - static final private boolean jj_3R_66() { - Token xsp; - xsp = jj_scanpos; - if (jj_3_124()) { - jj_scanpos = xsp; - if (jj_3_125()) return true; - } + static final private boolean jj_3_125() { + if (jj_3R_66()) return true; return false; } - static final private boolean jj_3_124() { - if (jj_scan_token(DQUOTE)) return true; - if (jj_scan_token(INIT)) return true; - if (jj_scan_token(DQUOTE)) return true; + static final private boolean jj_3R_64() { + if (jj_scan_token(CUMUL)) return true; + if (jj_scan_token(LE)) return true; + if (jj_3R_35()) return true; return false; } - static final private boolean jj_3_77() { - if (jj_scan_token(IMPLIES)) return true; - if (jj_3R_52()) return true; + static final private boolean jj_3_150() { + if (jj_3R_75()) return true; return false; } - static final private boolean jj_3R_41() { - Token xsp; - xsp = jj_scanpos; - if (jj_3_46()) { - jj_scanpos = xsp; - if (jj_3_47()) return true; - } + static final private boolean jj_3_7() { + if (jj_3R_29()) return true; return false; } - static final private boolean jj_3_145() { - Token xsp; - xsp = jj_scanpos; - if (jj_3_146()) { - jj_scanpos = xsp; - if (jj_3_147()) return true; - } - if (jj_3R_76()) return true; + static final private boolean jj_3_129() { + if (jj_scan_token(LBRACE)) return true; + if (jj_scan_token(MAX)) return true; + if (jj_scan_token(RBRACE)) return true; return false; } - static final private boolean jj_3_46() { - if (jj_scan_token(LPARENTH)) return true; - if (jj_3R_42()) return true; - if (jj_scan_token(EQ)) return true; + static final private boolean jj_3_114() { if (jj_3R_35()) return true; - if (jj_scan_token(RPARENTH)) return true; - return false; - } - - static final private boolean jj_3_14() { - if (jj_3R_34()) return true; - return false; - } - - static final private boolean jj_3_7() { - if (jj_3R_29()) return true; return false; } - static final private boolean jj_3R_88() { + static final private boolean jj_3R_90() { if (jj_3R_52()) return true; Token xsp; xsp = jj_scanpos; @@ -4955,13 +5105,8 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_65() { - if (jj_scan_token(S)) return true; - return false; - } - - static final private boolean jj_3_144() { - if (jj_scan_token(MINUS)) return true; + static final private boolean jj_3_132() { + if (jj_3R_68()) return true; return false; } @@ -4975,8 +5120,8 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_59() { - if (jj_3R_88()) return true; + static final private boolean jj_3R_61() { + if (jj_3R_90()) return true; return false; } @@ -4991,29 +5136,8 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_75() { - if (jj_3R_76()) return true; - Token xsp; - while (true) { - xsp = jj_scanpos; - if (jj_3_145()) { jj_scanpos = xsp; break; } - } - return false; - } - - static final private boolean jj_3_143() { - if (jj_scan_token(PLUS)) return true; - return false; - } - - static final private boolean jj_3_142() { - Token xsp; - xsp = jj_scanpos; - if (jj_3_143()) { - jj_scanpos = xsp; - if (jj_3_144()) return true; - } - if (jj_3R_75()) return true; + static final private boolean jj_3_124() { + if (jj_3R_65()) return true; return false; } @@ -5036,18 +5160,18 @@ public class PrismParser implements PrismParserConstants { } static final private boolean jj_3R_34() { - if (jj_3R_59()) return true; + if (jj_3R_61()) return true; return false; } - static final private boolean jj_3_5() { - if (jj_3R_27()) return true; + static final private boolean jj_3_147() { + if (jj_scan_token(DOTS)) return true; + if (jj_3R_75()) return true; return false; } - static final private boolean jj_3R_64() { - if (jj_scan_token(FUTURE)) return true; - if (jj_3R_59()) return true; + static final private boolean jj_3_5() { + if (jj_3R_27()) return true; return false; } @@ -5076,6 +5200,47 @@ public class PrismParser implements PrismParserConstants { return false; } + static final private boolean jj_3_127() { + Token xsp; + xsp = jj_scanpos; + if (jj_3_128()) { + jj_scanpos = xsp; + if (jj_3_129()) return true; + } + return false; + } + + static final private boolean jj_3_128() { + if (jj_scan_token(LBRACE)) return true; + if (jj_scan_token(MIN)) return true; + if (jj_scan_token(RBRACE)) return true; + return false; + } + + static final private boolean jj_3_130() { + if (jj_scan_token(LBRACE)) return true; + if (jj_3R_61()) return true; + if (jj_scan_token(RBRACE)) return true; + Token xsp; + while (true) { + xsp = jj_scanpos; + if (jj_3_127()) { jj_scanpos = xsp; break; } + } + return false; + } + + static final private boolean jj_3_123() { + if (jj_3R_64()) return true; + return false; + } + + static final private boolean jj_3_113() { + if (jj_scan_token(DQUOTE)) return true; + if (jj_3R_36()) return true; + if (jj_scan_token(DQUOTE)) return true; + return false; + } + static final private boolean jj_3_75() { if (jj_3R_36()) return true; return false; @@ -5086,8 +5251,23 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3_117() { - if (jj_3R_65()) return true; + static final private boolean jj_3_122() { + if (jj_scan_token(RMAX)) return true; + if (jj_scan_token(EQ)) return true; + if (jj_scan_token(QMARK)) return true; + return false; + } + + static final private boolean jj_3_145() { + if (jj_scan_token(DOTS)) return true; + if (jj_3R_75()) return true; + return false; + } + + static final private boolean jj_3_121() { + if (jj_scan_token(RMIN)) return true; + if (jj_scan_token(EQ)) return true; + if (jj_scan_token(QMARK)) return true; return false; } @@ -5098,10 +5278,17 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_63() { - if (jj_scan_token(INST)) return true; + static final private boolean jj_3_119() { + if (jj_scan_token(MAX)) return true; if (jj_scan_token(EQ)) return true; - if (jj_3R_35()) return true; + if (jj_scan_token(QMARK)) return true; + return false; + } + + static final private boolean jj_3_118() { + if (jj_scan_token(MIN)) return true; + if (jj_scan_token(EQ)) return true; + if (jj_scan_token(QMARK)) return true; return false; } @@ -5112,12 +5299,55 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_73() { - if (jj_3R_75()) return true; + static final private boolean jj_3_116() { + if (jj_3R_55()) return true; + if (jj_3R_35()) return true; + return false; + } + + static final private boolean jj_3_117() { + if (jj_scan_token(EQ)) return true; + if (jj_scan_token(QMARK)) return true; + return false; + } + + static final private boolean jj_3_115() { + if (jj_scan_token(LBRACE)) return true; Token xsp; - while (true) { - xsp = jj_scanpos; - if (jj_3_142()) { jj_scanpos = xsp; break; } + xsp = jj_scanpos; + if (jj_3_113()) { + jj_scanpos = xsp; + if (jj_3_114()) return true; + } + if (jj_scan_token(RBRACE)) return true; + return false; + } + + static final private boolean jj_3_120() { + if (jj_scan_token(R)) return true; + Token xsp; + xsp = jj_scanpos; + if (jj_3_115()) jj_scanpos = xsp; + xsp = jj_scanpos; + if (jj_3_116()) { + jj_scanpos = xsp; + if (jj_3_117()) { + jj_scanpos = xsp; + if (jj_3_118()) { + jj_scanpos = xsp; + if (jj_3_119()) return true; + } + } + } + return false; + } + + static final private boolean jj_3R_63() { + Token xsp; + xsp = jj_scanpos; + if (jj_3_131()) { + jj_scanpos = xsp; + if (jj_3_132()) return true; } return false; } @@ -5131,11 +5361,46 @@ public class PrismParser implements PrismParserConstants { return false; } + static final private boolean jj_3_131() { + Token xsp; + xsp = jj_scanpos; + if (jj_3_120()) { + jj_scanpos = xsp; + if (jj_3_121()) { + jj_scanpos = xsp; + if (jj_3_122()) return true; + } + } + if (jj_scan_token(LBRACKET)) return true; + xsp = jj_scanpos; + if (jj_3_123()) { + jj_scanpos = xsp; + if (jj_3_124()) { + jj_scanpos = xsp; + if (jj_3_125()) { + jj_scanpos = xsp; + if (jj_3_126()) return true; + } + } + } + xsp = jj_scanpos; + if (jj_3_130()) jj_scanpos = xsp; + if (jj_scan_token(RBRACKET)) return true; + return false; + } + static final private boolean jj_3_3() { if (jj_3R_25()) return true; return false; } + static final private boolean jj_3_110() { + if (jj_scan_token(LBRACE)) return true; + if (jj_3R_61()) return true; + if (jj_scan_token(RBRACE)) return true; + return false; + } + static final private boolean jj_3R_51() { Token xsp; xsp = jj_scanpos; @@ -5153,27 +5418,12 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3_116() { - if (jj_3R_64()) return true; - return false; - } - - static final private boolean jj_3R_62() { - if (jj_scan_token(CUMUL)) return true; - if (jj_scan_token(LE)) return true; - if (jj_3R_35()) return true; - return false; - } - - static final private boolean jj_3_120() { - if (jj_scan_token(LBRACE)) return true; - if (jj_scan_token(MAX)) return true; - if (jj_scan_token(RBRACE)) return true; - return false; - } - - static final private boolean jj_3_141() { - if (jj_3R_73()) return true; + static final private boolean jj_3_146() { + if (jj_scan_token(COMMA)) return true; + if (jj_3R_75()) return true; + Token xsp; + xsp = jj_scanpos; + if (jj_3_147()) jj_scanpos = xsp; return false; } @@ -5184,13 +5434,17 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3_105() { - if (jj_3R_35()) return true; + static final private boolean jj_3_112() { + if (jj_3R_63()) return true; return false; } - static final private boolean jj_3_123() { - if (jj_3R_66()) return true; + static final private boolean jj_3_105() { + if (jj_scan_token(LBRACKET)) return true; + if (jj_3R_35()) return true; + if (jj_scan_token(COMMA)) return true; + if (jj_3R_35()) return true; + if (jj_scan_token(RBRACKET)) return true; return false; } @@ -5204,8 +5458,31 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3_115() { - if (jj_3R_63()) return true; + static final private boolean jj_3_149() { + if (jj_3R_75()) return true; + if (jj_3R_76()) return true; + if (jj_3R_75()) return true; + Token xsp; + xsp = jj_scanpos; + if (jj_3_145()) jj_scanpos = xsp; + while (true) { + xsp = jj_scanpos; + if (jj_3_146()) { jj_scanpos = xsp; break; } + } + return false; + } + + static final private boolean jj_3_109() { + if (jj_scan_token(S)) return true; + if (jj_scan_token(EQ)) return true; + if (jj_scan_token(QMARK)) return true; + return false; + } + + static final private boolean jj_3_108() { + if (jj_scan_token(S)) return true; + if (jj_3R_55()) return true; + if (jj_3R_35()) return true; return false; } @@ -5222,7 +5499,7 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_85() { + static final private boolean jj_3R_87() { Token xsp; xsp = jj_scanpos; if (jj_3_41()) { @@ -5237,9 +5514,59 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3_138() { - if (jj_scan_token(DOTS)) return true; - if (jj_3R_73()) return true; + static final private boolean jj_3R_91() { + Token xsp; + xsp = jj_scanpos; + if (jj_3_148()) { + jj_scanpos = xsp; + if (jj_3_149()) { + jj_scanpos = xsp; + if (jj_3_150()) return true; + } + } + return false; + } + + static final private boolean jj_3_148() { + if (jj_3R_75()) return true; + if (jj_3R_55()) return true; + if (jj_3R_75()) return true; + return false; + } + + static final private boolean jj_3_104() { + if (jj_scan_token(GE)) return true; + if (jj_3R_35()) return true; + return false; + } + + static final private boolean jj_3R_62() { + Token xsp; + xsp = jj_scanpos; + if (jj_3_111()) { + jj_scanpos = xsp; + if (jj_3_112()) return true; + } + return false; + } + + static final private boolean jj_3_111() { + Token xsp; + xsp = jj_scanpos; + if (jj_3_108()) { + jj_scanpos = xsp; + if (jj_3_109()) return true; + } + if (jj_scan_token(LBRACKET)) return true; + if (jj_3R_61()) return true; + xsp = jj_scanpos; + if (jj_3_110()) jj_scanpos = xsp; + if (jj_scan_token(RBRACKET)) return true; + return false; + } + + static final private boolean jj_3_107() { + if (jj_scan_token(GLOB)) return true; return false; } @@ -5279,50 +5606,9 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3_118() { - Token xsp; - xsp = jj_scanpos; - if (jj_3_119()) { - jj_scanpos = xsp; - if (jj_3_120()) return true; - } - return false; - } - - static final private boolean jj_3_119() { - if (jj_scan_token(LBRACE)) return true; - if (jj_scan_token(MIN)) return true; - if (jj_scan_token(RBRACE)) return true; - return false; - } - - static final private boolean jj_3_121() { - if (jj_scan_token(LBRACE)) return true; - if (jj_3R_59()) return true; - if (jj_scan_token(RBRACE)) return true; - Token xsp; - while (true) { - xsp = jj_scanpos; - if (jj_3_118()) { jj_scanpos = xsp; break; } - } - return false; - } - - static final private boolean jj_3_114() { - if (jj_3R_62()) return true; - return false; - } - - static final private boolean jj_3_104() { - if (jj_scan_token(DQUOTE)) return true; - if (jj_3R_36()) return true; - if (jj_scan_token(DQUOTE)) return true; - return false; - } - static final private boolean jj_3R_50() { if (jj_scan_token(LPARENTH)) return true; - if (jj_3R_84()) return true; + if (jj_3R_86()) return true; if (jj_scan_token(RPARENTH)) return true; return false; } @@ -5332,118 +5618,42 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3_113() { - if (jj_scan_token(RMAX)) return true; - if (jj_scan_token(EQ)) return true; - if (jj_scan_token(QMARK)) return true; - return false; - } - - static final private boolean jj_3_112() { - if (jj_scan_token(RMIN)) return true; - if (jj_scan_token(EQ)) return true; - if (jj_scan_token(QMARK)) return true; - return false; - } - - static final private boolean jj_3_136() { - if (jj_scan_token(DOTS)) return true; - if (jj_3R_73()) return true; - return false; - } - - static final private boolean jj_3_110() { - if (jj_scan_token(MAX)) return true; - if (jj_scan_token(EQ)) return true; - if (jj_scan_token(QMARK)) return true; - return false; - } - - static final private boolean jj_3_109() { - if (jj_scan_token(MIN)) return true; - if (jj_scan_token(EQ)) return true; - if (jj_scan_token(QMARK)) return true; + static final private boolean jj_3R_83() { + if (jj_scan_token(REG_DOUBLE)) return true; return false; } - static final private boolean jj_3_107() { - if (jj_3R_55()) return true; - if (jj_3R_35()) return true; + static final private boolean jj_3_185() { + if (jj_scan_token(LE)) return true; return false; } - static final private boolean jj_3_108() { - if (jj_scan_token(EQ)) return true; - if (jj_scan_token(QMARK)) return true; + static final private boolean jj_3_144() { + if (jj_scan_token(NOT)) return true; return false; } static final private boolean jj_3_106() { - if (jj_scan_token(LBRACE)) return true; - Token xsp; - xsp = jj_scanpos; - if (jj_3_104()) { - jj_scanpos = xsp; - if (jj_3_105()) return true; - } - if (jj_scan_token(RBRACE)) return true; - return false; - } - - static final private boolean jj_3_111() { - if (jj_scan_token(R)) return true; - Token xsp; - xsp = jj_scanpos; - if (jj_3_106()) jj_scanpos = xsp; - xsp = jj_scanpos; - if (jj_3_107()) { - jj_scanpos = xsp; - if (jj_3_108()) { - jj_scanpos = xsp; - if (jj_3_109()) { - jj_scanpos = xsp; - if (jj_3_110()) return true; - } - } - } + if (jj_scan_token(FUTURE)) return true; return false; } - static final private boolean jj_3R_61() { + static final private boolean jj_3R_74() { Token xsp; xsp = jj_scanpos; - if (jj_3_122()) { - jj_scanpos = xsp; - if (jj_3_123()) return true; - } + if (jj_3_144()) jj_scanpos = xsp; + if (jj_3R_91()) return true; return false; } - static final private boolean jj_3_122() { + static final private boolean jj_3R_60() { Token xsp; xsp = jj_scanpos; - if (jj_3_111()) { - jj_scanpos = xsp; - if (jj_3_112()) { - jj_scanpos = xsp; - if (jj_3_113()) return true; - } - } - if (jj_scan_token(LBRACKET)) return true; - xsp = jj_scanpos; - if (jj_3_114()) { - jj_scanpos = xsp; - if (jj_3_115()) { + if (jj_3_106()) { jj_scanpos = xsp; - if (jj_3_116()) { - jj_scanpos = xsp; - if (jj_3_117()) return true; - } - } + if (jj_3_107()) return true; } - xsp = jj_scanpos; - if (jj_3_121()) jj_scanpos = xsp; - if (jj_scan_token(RBRACKET)) return true; + if (jj_3R_61()) return true; return false; } @@ -5468,29 +5678,35 @@ public class PrismParser implements PrismParserConstants { if (jj_scan_token(RBRACKET)) return true; if (jj_3R_35()) return true; if (jj_scan_token(RARROW)) return true; - if (jj_3R_85()) return true; + if (jj_3R_87()) return true; if (jj_scan_token(SEMICOLON)) return true; return false; } - static final private boolean jj_3_101() { - if (jj_scan_token(LBRACE)) return true; - if (jj_3R_59()) return true; - if (jj_scan_token(RBRACE)) return true; + static final private boolean jj_3_184() { + if (jj_scan_token(GE)) return true; return false; } - static final private boolean jj_3_137() { - if (jj_scan_token(COMMA)) return true; - if (jj_3R_73()) return true; - Token xsp; - xsp = jj_scanpos; - if (jj_3_138()) jj_scanpos = xsp; + static final private boolean jj_3_103() { + if (jj_scan_token(LE)) return true; + if (jj_3R_35()) return true; return false; } - static final private boolean jj_3_103() { - if (jj_3R_61()) return true; + static final private boolean jj_3R_82() { + if (jj_scan_token(REG_INT)) return true; + return false; + } + + static final private boolean jj_3_183() { + if (jj_scan_token(LT)) return true; + return false; + } + + static final private boolean jj_3_143() { + if (jj_scan_token(AND)) return true; + if (jj_3R_74()) return true; return false; } @@ -5499,20 +5715,37 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3_140() { - if (jj_3R_73()) return true; - if (jj_3R_74()) return true; - if (jj_3R_73()) return true; + static final private boolean jj_3_182() { + if (jj_scan_token(GT)) return true; + return false; + } + + static final private boolean jj_3R_55() { Token xsp; xsp = jj_scanpos; - if (jj_3_136()) jj_scanpos = xsp; - while (true) { - xsp = jj_scanpos; - if (jj_3_137()) { jj_scanpos = xsp; break; } + if (jj_3_182()) { + jj_scanpos = xsp; + if (jj_3_183()) { + jj_scanpos = xsp; + if (jj_3_184()) { + jj_scanpos = xsp; + if (jj_3_185()) return true; + } + } } return false; } + static final private boolean jj_3_102() { + if (jj_scan_token(GLOB)) return true; + return false; + } + + static final private boolean jj_3_181() { + if (jj_scan_token(NE)) return true; + return false; + } + static final private boolean jj_3_72() { if (jj_3R_50()) return true; return false; @@ -5524,7 +5757,7 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_86() { + static final private boolean jj_3R_88() { Token xsp; xsp = jj_scanpos; if (jj_3_71()) { @@ -5550,7 +5783,7 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3_98() { + static final private boolean jj_3_100() { if (jj_scan_token(LBRACKET)) return true; if (jj_3R_35()) return true; if (jj_scan_token(COMMA)) return true; @@ -5559,17 +5792,28 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3_100() { - if (jj_scan_token(S)) return true; + static final private boolean jj_3_180() { if (jj_scan_token(EQ)) return true; - if (jj_scan_token(QMARK)) return true; return false; } - static final private boolean jj_3_99() { - if (jj_scan_token(S)) return true; - if (jj_3R_55()) return true; - if (jj_3R_35()) return true; + static final private boolean jj_3R_76() { + Token xsp; + xsp = jj_scanpos; + if (jj_3_180()) { + jj_scanpos = xsp; + if (jj_3_181()) return true; + } + return false; + } + + static final private boolean jj_3R_92() { + if (jj_3R_74()) return true; + Token xsp; + while (true) { + xsp = jj_scanpos; + if (jj_3_143()) { jj_scanpos = xsp; break; } + } return false; } @@ -5579,48 +5823,43 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_89() { - Token xsp; - xsp = jj_scanpos; - if (jj_3_139()) { - jj_scanpos = xsp; - if (jj_3_140()) { - jj_scanpos = xsp; - if (jj_3_141()) return true; - } - } + static final private boolean jj_3_167() { + if (jj_scan_token(CEIL)) return true; return false; } - static final private boolean jj_3_139() { - if (jj_3R_73()) return true; - if (jj_3R_55()) return true; - if (jj_3R_73()) return true; + static final private boolean jj_3_101() { + if (jj_scan_token(FUTURE)) return true; return false; } - static final private boolean jj_3R_60() { + static final private boolean jj_3R_59() { Token xsp; xsp = jj_scanpos; - if (jj_3_102()) { + if (jj_3_101()) { jj_scanpos = xsp; - if (jj_3_103()) return true; + if (jj_3_102()) return true; } - return false; - } - - static final private boolean jj_3_102() { - Token xsp; xsp = jj_scanpos; - if (jj_3_99()) { + if (jj_3_103()) { jj_scanpos = xsp; - if (jj_3_100()) return true; + if (jj_3_104()) { + jj_scanpos = xsp; + if (jj_3_105()) return true; } - if (jj_scan_token(LBRACKET)) return true; - if (jj_3R_59()) return true; - xsp = jj_scanpos; - if (jj_3_101()) jj_scanpos = xsp; - if (jj_scan_token(RBRACKET)) return true; + } + if (jj_3R_61()) return true; + return false; + } + + static final private boolean jj_3_142() { + if (jj_scan_token(OR)) return true; + if (jj_3R_72()) return true; + return false; + } + + static final private boolean jj_3R_42() { + if (jj_scan_token(REG_IDENTPRIME)) return true; return false; } @@ -5675,14 +5914,14 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3_97() { + static final private boolean jj_3_99() { if (jj_scan_token(GE)) return true; if (jj_3R_35()) return true; return false; } - static final private boolean jj_3R_81() { - if (jj_scan_token(REG_DOUBLE)) return true; + static final private boolean jj_3R_36() { + if (jj_scan_token(REG_IDENT)) return true; return false; } @@ -5724,7 +5963,7 @@ public class PrismParser implements PrismParserConstants { private static void jj_la1_2() { jj_la1_2 = new int[] {}; } - static final private JJCalls[] jj_2_rtns = new JJCalls[176]; + static final private JJCalls[] jj_2_rtns = new JJCalls[185]; static private boolean jj_rescan = false; static private int jj_gc = 0; @@ -5968,7 +6207,7 @@ public class PrismParser implements PrismParserConstants { static final private void jj_rescan_token() { jj_rescan = true; - for (int i = 0; i < 176; i++) { + for (int i = 0; i < 185; i++) { try { JJCalls p = jj_2_rtns[i]; do { @@ -6151,6 +6390,15 @@ public class PrismParser implements PrismParserConstants { case 173: jj_3_174(); break; case 174: jj_3_175(); break; case 175: jj_3_176(); break; + case 176: jj_3_177(); break; + case 177: jj_3_178(); break; + case 178: jj_3_179(); break; + case 179: jj_3_180(); break; + case 180: jj_3_181(); break; + case 181: jj_3_182(); break; + case 182: jj_3_183(); break; + case 183: jj_3_184(); break; + case 184: jj_3_185(); break; } } p = p.next; diff --git a/prism/src/parser/PrismParser.jj b/prism/src/parser/PrismParser.jj index 77e677a0..d0f328a5 100644 --- a/prism/src/parser/PrismParser.jj +++ b/prism/src/parser/PrismParser.jj @@ -1418,7 +1418,7 @@ void PCTLProb() : ( {relOp="max=";} ) ) // path formula bit - ( PCTLProbNext() | PCTLProbBoundedUntil() | PCTLProbUntil() ) + ( PCTLProbNext() | PCTLProbBoundedUntil() | PCTLProbUntil() | PCTLProbBoundedFutureGlobal() | PCTLProbFutureGlobal() ) ( tf= PCTLFormula() (( tfmin= ) | ( tfmax= ))* )? ) @@ -1527,6 +1527,71 @@ void PCTLProbUntil() : } } +// pctl bounded future (eventually) or global + +void PCTLProbBoundedFutureGlobal() : +{ + Token tfuture = null; // detects if a future formula is used + Token tglobal = null; // detects if a global formula is used + Token tle = null; // detects if a <= time bound is used + Token tge = null; // detects if a >= time bound is used + Token tr = null; // detects if a range time bound is used +} +{ + ( (tfuture=|tglobal=) ((tle= Expression()) | (tge= Expression()) | (tr= Expression() Expression() )) PCTLFormula() ) + { + PCTLFormula f = null; + Expression lb, ub; + PCTLFormula u; + + // pop operand off stack + f = (PCTLFormula)stack.pop(); + // U<=ub + if (tle != null) { + ub = (Expression)stack.pop(); + if (tfuture != null) u = new PCTLProbBoundedFuture(f, null, ub); + else u = new PCTLProbBoundedGlobal(f, null, ub); + } + // U>=lb + else if (tge != null) { + lb = (Expression)stack.pop(); + if (tfuture != null) u = new PCTLProbBoundedFuture(f, lb, null); + else u = new PCTLProbBoundedGlobal(f, lb, null); + } + // U[lb,ub] + else { + ub = (Expression)stack.pop(); + lb = (Expression)stack.pop(); + if (tfuture != null) u = new PCTLProbBoundedFuture(f, lb, ub); + else u = new PCTLProbBoundedGlobal(f, lb, ub); + } + // push result onto stack + stack.push(u); + } +} + +// pctl future (eventually) or globally + +void PCTLProbFutureGlobal() : +{ + Token tfuture = null; // detects if a future formula is used + Token tglobal = null; // detects if a global formula is used +} +{ + ( (tfuture=|tglobal=) PCTLFormula() ) + { + PCTLFormula f; + PCTLFormula u; + + // create PCTLProbFuture/PCTLProbGlobal object + f = (PCTLFormula)stack.pop(); + if (tfuture != null) u = new PCTLProbFuture(f); + else u = new PCTLProbGlobal(f); + // push result onto stack + stack.push(u); + } +} + // pctl steady state (actually only csl - not pctl at all) void PCTLSS() : diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index 2b06abdf..769dc96c 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -494,6 +494,14 @@ public class NondetModelChecker implements ModelChecker probs = checkPCTLProbBoundedUntil((PCTLProbBoundedUntil)f, min); else if (f instanceof PCTLProbUntil) probs = checkPCTLProbUntil((PCTLProbUntil)f, pe, p, min); + else if (f instanceof PCTLProbBoundedFuture) + probs = checkPCTLProbBoundedFuture((PCTLProbBoundedFuture)f, min); + else if (f instanceof PCTLProbFuture) + probs = checkPCTLProbFuture((PCTLProbFuture)f, pe, p, min); + else if (f instanceof PCTLProbBoundedGlobal) + probs = checkPCTLProbBoundedGlobal((PCTLProbBoundedGlobal)f, min); + else if (f instanceof PCTLProbGlobal) + probs = checkPCTLProbGlobal((PCTLProbGlobal)f, pe, p, min); else throw new PrismException("Unrecognised path operator in P[] formula"); } @@ -964,9 +972,10 @@ public class NondetModelChecker implements ModelChecker } // if p is 0 or 1 and precomputation algorithms are enabled, compute probabilities qualitatively - if (pe != null && ((p==0) || (p==1)) & precomp) { + if (pe != null && ((p==0) || (p==1)) && precomp) { mainLog.print("\nWarning: probability bound in formula is " + p + " so exact probabilities may not be computed\n"); - probs = computeUntilProbsQual(trans01, b1, b2, p, min); + // for fairness, we compute max here + probs = computeUntilProbsQual(trans01, b1, b2, min&&!fairness); } // otherwise actually compute probabilities else { @@ -994,6 +1003,56 @@ public class NondetModelChecker implements ModelChecker return probs; } + + // bounded future (eventually) + // F<=k phi == true U<=k phi + + private StateProbs checkPCTLProbBoundedFuture(PCTLProbBoundedFuture pctl, boolean min) throws PrismException + { + PCTLProbBoundedUntil pctlBUntil; + pctlBUntil = new PCTLProbBoundedUntil(new PCTLExpression(new ExpressionTrue()), pctl.getOperand(), pctl.getLowerBound(), pctl.getUpperBound()); + return checkPCTLProbBoundedUntil(pctlBUntil, min); + } + + // future (eventually) + // F phi == true U phi + + private StateProbs checkPCTLProbFuture(PCTLProbFuture pctl, Expression pe, double p, boolean min) throws PrismException + { + PCTLProbUntil pctlUntil; + pctlUntil = new PCTLProbUntil(new PCTLExpression(new ExpressionTrue()), pctl.getOperand()); + return checkPCTLProbUntil(pctlUntil, pe, p, min); + } + + // bounded global (always) + // F<=k phi == true U<=k phi + // P(G<=k phi) == 1-P(true U<=k !phi) + // Pmin(G<=k phi) == 1-Pmax(true U<=k !phi) + + private StateProbs checkPCTLProbBoundedGlobal(PCTLProbBoundedGlobal pctl, boolean min) throws PrismException + { + PCTLProbBoundedUntil pctlBUntil; + StateProbs probs; + pctlBUntil = new PCTLProbBoundedUntil(new PCTLExpression(new ExpressionTrue()), new PCTLNot(pctl.getOperand()), pctl.getLowerBound(), pctl.getUpperBound()); + probs = checkPCTLProbBoundedUntil(pctlBUntil, !min); + probs.subtractFromOne(); + return probs; + } + + // global (always) + // G phi == !(true U !phi) + // P(G phi) == 1-P(true U !phi) + // Pmin(G phi) == 1-Pmax(true U !phi) + + private StateProbs checkPCTLProbGlobal(PCTLProbGlobal pctl, Expression pe, double p, boolean min) throws PrismException + { + PCTLProbUntil pctlUntil; + StateProbs probs; + pctlUntil = new PCTLProbUntil(new PCTLExpression(new ExpressionTrue()), new PCTLNot(pctl.getOperand())); + probs = checkPCTLProbUntil(pctlUntil, pe, p, !min); + probs.subtractFromOne(); + return probs; + } // reach reward @@ -1187,9 +1246,11 @@ public class NondetModelChecker implements ModelChecker } // compute probabilities for until (for qualitative properties) - // note: this func needs to know 'min', 'fairness' and 'p' - private StateProbs computeUntilProbsQual(JDDNode tr01, JDDNode b1, JDDNode b2, double p, boolean min) + // note: this function doesn't need to know anything about fairness + // it is just told whether to compute min or max probabilities + + private StateProbs computeUntilProbsQual(JDDNode tr01, JDDNode b1, JDDNode b2, boolean min) { JDDNode yes = null, no = null, maybe; StateProbs probs = null; @@ -1212,9 +1273,8 @@ public class NondetModelChecker implements ModelChecker maybe = JDD.Constant(0); } else { - // note: if using fairness, we're always looking for the max probabilities // min - if (min&&!fairness) { + if (min) { // no: "min prob = 0" equates to "there exists an adversary prob equals 0" no = PrismMTBDD.Prob0E(tr01, reach, nondetMask, allDDRowVars, allDDColVars, allDDNondetVars, b1, b2); // yes: "min prob = 1" equates to "for all adversaries prob equals 1" @@ -1260,41 +1320,15 @@ public class NondetModelChecker implements ModelChecker JDD.Ref(yes); probs = new StateProbsMTBDD(yes, model); } - // p = 0 - else if (p == 0) { - if (!(min && fairness)) { - // anything that's unknown but definitely > 0 - // may as well be 1 - JDD.Ref(yes); - JDD.Ref(maybe); - probs = new StateProbsMTBDD(JDD.Or(yes, maybe), model); - } - else { - // have to be careful here though because actually solving the dual problem - // solving min so must be checking for > 0 - // for states in maybe, p is in (0,1) and 1-p > 0 - // so just set them to 0 and will become 1 which is still > 0 - JDD.Ref(yes); - probs = new StateProbsMTBDD(yes, model); - } - } - // p = 1 + // otherwise we set the probabilities for maybe states to be 0.5 + // (actual probabilities for these states are unknown but definitely >0 and <1) + // (this is safe because the results of this function will only be used to compare against 0/1 bounds) + // (this is not entirely elegant but is simpler and less error prone than + // trying to work out whether to use 0/1 for all case of min/max, fairness, future/global, etc.) else { - if (!(min && fairness)) { - // anything that's unknown but definitely < 1 - // may as well be 0 - JDD.Ref(yes); - probs = new StateProbsMTBDD(yes, model); - } - else { - // have to be careful here though because actually solving the dual problem - // solving min so must be checking for >= 1 - // for states in maybe, p is in (0,1) and 1-p not >= 1 - // so just set them to 1 and will become 0 which is still not >= 1 - JDD.Ref(yes); - JDD.Ref(maybe); - probs = new StateProbsMTBDD(JDD.Or(yes, maybe), model); - } + JDD.Ref(yes); + JDD.Ref(maybe); + probs = new StateProbsMTBDD(JDD.Apply(JDD.PLUS, yes, JDD.Apply(JDD.TIMES, maybe, JDD.Constant(0.5))), model); } // derefs diff --git a/prism/src/prism/ProbModelChecker.java b/prism/src/prism/ProbModelChecker.java index 52d08391..200f556e 100644 --- a/prism/src/prism/ProbModelChecker.java +++ b/prism/src/prism/ProbModelChecker.java @@ -507,6 +507,14 @@ public class ProbModelChecker implements ModelChecker probs = checkPCTLProbBoundedUntil((PCTLProbBoundedUntil)f); else if (f instanceof PCTLProbUntil) probs = checkPCTLProbUntil((PCTLProbUntil)f, pe, p); + else if (f instanceof PCTLProbBoundedFuture) + probs = checkPCTLProbBoundedFuture((PCTLProbBoundedFuture)f); + else if (f instanceof PCTLProbFuture) + probs = checkPCTLProbFuture((PCTLProbFuture)f, pe, p); + else if (f instanceof PCTLProbBoundedGlobal) + probs = checkPCTLProbBoundedGlobal((PCTLProbBoundedGlobal)f); + else if (f instanceof PCTLProbGlobal) + probs = checkPCTLProbGlobal((PCTLProbGlobal)f, pe, p); else throw new PrismException("Unrecognised path operator in P[] formula"); } @@ -937,7 +945,7 @@ public class ProbModelChecker implements ModelChecker // compute probabilities // if prob bound is 0 or 1 and precomputation algorithms are enabled, compute probabilities qualitatively - if (pe != null && ((p==0) || (p==1)) & precomp) { + if (pe != null && ((p==0) || (p==1)) && precomp) { mainLog.print("\nWarning: Probability bound in formula is " + p + " so exact probabilities may not be computed\n"); probs = computeUntilProbsQual(trans01, b1, b2, p); } @@ -959,6 +967,54 @@ public class ProbModelChecker implements ModelChecker return probs; } + + // bounded future (eventually) + // F<=k phi == true U<=k phi + + private StateProbs checkPCTLProbBoundedFuture(PCTLProbBoundedFuture pctl) throws PrismException + { + PCTLProbBoundedUntil pctlBUntil; + pctlBUntil = new PCTLProbBoundedUntil(new PCTLExpression(new ExpressionTrue()), pctl.getOperand(), pctl.getLowerBound(), pctl.getUpperBound()); + return checkPCTLProbBoundedUntil(pctlBUntil); + } + + // future (eventually) + // F phi == true U phi + + private StateProbs checkPCTLProbFuture(PCTLProbFuture pctl, Expression pe, double p) throws PrismException + { + PCTLProbUntil pctlUntil; + pctlUntil = new PCTLProbUntil(new PCTLExpression(new ExpressionTrue()), pctl.getOperand()); + return checkPCTLProbUntil(pctlUntil, pe, p); + } + + // bounded global (always) + // F<=k phi == true U<=k phi + // P(G<=k phi) == 1-P(true U<=k !phi) + + private StateProbs checkPCTLProbBoundedGlobal(PCTLProbBoundedGlobal pctl) throws PrismException + { + PCTLProbBoundedUntil pctlBUntil; + StateProbs probs; + pctlBUntil = new PCTLProbBoundedUntil(new PCTLExpression(new ExpressionTrue()), new PCTLNot(pctl.getOperand()), pctl.getLowerBound(), pctl.getUpperBound()); + probs = checkPCTLProbBoundedUntil(pctlBUntil); + probs.subtractFromOne(); + return probs; + } + + // global (always) + // G phi == !(true U !phi) + // P(G phi) == 1-P(true U !phi) + + private StateProbs checkPCTLProbGlobal(PCTLProbGlobal pctl, Expression pe, double p) throws PrismException + { + PCTLProbUntil pctlUntil; + StateProbs probs; + pctlUntil = new PCTLProbUntil(new PCTLExpression(new ExpressionTrue()), new PCTLNot(pctl.getOperand())); + probs = checkPCTLProbUntil(pctlUntil, pe, p); + probs.subtractFromOne(); + return probs; + } // reach reward diff --git a/prism/src/prism/StochModelChecker.java b/prism/src/prism/StochModelChecker.java index bb09f21e..51cecec7 100644 --- a/prism/src/prism/StochModelChecker.java +++ b/prism/src/prism/StochModelChecker.java @@ -531,6 +531,14 @@ public class StochModelChecker implements ModelChecker probs = checkPCTLProbBoundedUntil((PCTLProbBoundedUntil)f); else if (f instanceof PCTLProbUntil) probs = checkPCTLProbUntil((PCTLProbUntil)f, pe, p); + else if (f instanceof PCTLProbBoundedFuture) + probs = checkPCTLProbBoundedFuture((PCTLProbBoundedFuture)f); + else if (f instanceof PCTLProbFuture) + probs = checkPCTLProbFuture((PCTLProbFuture)f, pe, p); + else if (f instanceof PCTLProbBoundedGlobal) + probs = checkPCTLProbBoundedGlobal((PCTLProbBoundedGlobal)f); + else if (f instanceof PCTLProbGlobal) + probs = checkPCTLProbGlobal((PCTLProbGlobal)f, pe, p); else throw new PrismException("Unrecognised path operator in P[] formula"); } @@ -1404,7 +1412,7 @@ public class StochModelChecker implements ModelChecker mainLog.print(" states, b2 = " + JDD.GetNumMintermsString(b2, allDDRowVars.n()) + " states\n"); // if p is 0 or 1 and precomputation algorithms are enabled, compute probabilities qualitatively - if (pe != null && ((p==0) || (p==1)) & precomp) { + if (pe != null && ((p==0) || (p==1)) && precomp) { mainLog.print("\nWarning: probability bound in formula is " + p + " so exact probabilities may not be computed\n"); probs = computeUntilProbsQual(trans01, b1, b2, p); } @@ -1446,6 +1454,54 @@ public class StochModelChecker implements ModelChecker return probs; } + // bounded future (eventually) + // F[t1,t2] phi == true U[t1,t2] phi + + private StateProbs checkPCTLProbBoundedFuture(PCTLProbBoundedFuture pctl) throws PrismException + { + PCTLProbBoundedUntil pctlBUntil; + pctlBUntil = new PCTLProbBoundedUntil(new PCTLExpression(new ExpressionTrue()), pctl.getOperand(), pctl.getLowerBound(), pctl.getUpperBound()); + return checkPCTLProbBoundedUntil(pctlBUntil); + } + + // future (eventually) + // F phi == true U phi + + private StateProbs checkPCTLProbFuture(PCTLProbFuture pctl, Expression pe, double p) throws PrismException + { + PCTLProbUntil pctlUntil; + pctlUntil = new PCTLProbUntil(new PCTLExpression(new ExpressionTrue()), pctl.getOperand()); + return checkPCTLProbUntil(pctlUntil, pe, p); + } + + // bounded global (always) + // F<=k phi == true U<=k phi + // P(G<=k phi) == 1-P(true U<=k !phi) + + private StateProbs checkPCTLProbBoundedGlobal(PCTLProbBoundedGlobal pctl) throws PrismException + { + PCTLProbBoundedUntil pctlBUntil; + StateProbs probs; + pctlBUntil = new PCTLProbBoundedUntil(new PCTLExpression(new ExpressionTrue()), new PCTLNot(pctl.getOperand()), pctl.getLowerBound(), pctl.getUpperBound()); + probs = checkPCTLProbBoundedUntil(pctlBUntil); + probs.subtractFromOne(); + return probs; + } + + // global (always) + // G phi == !(true U !phi) + // P(G phi) == 1-P(true U !phi) + + private StateProbs checkPCTLProbGlobal(PCTLProbGlobal pctl, Expression pe, double p) throws PrismException + { + PCTLProbUntil pctlUntil; + StateProbs probs; + pctlUntil = new PCTLProbUntil(new PCTLExpression(new ExpressionTrue()), new PCTLNot(pctl.getOperand())); + probs = checkPCTLProbUntil(pctlUntil, pe, p); + probs.subtractFromOne(); + return probs; + } + // cumulative reward private StateProbs checkPCTLRewardCumul(PCTLRewardCumul pctl, JDDNode stateRewards, JDDNode transRewards) throws PrismException diff --git a/prism/src/simulator/SimulatorEngine.java b/prism/src/simulator/SimulatorEngine.java index bd7a293f..b93d13ac 100644 --- a/prism/src/simulator/SimulatorEngine.java +++ b/prism/src/simulator/SimulatorEngine.java @@ -2043,77 +2043,92 @@ public class SimulatorEngine allConstants.addValues(getConstants()); allConstants.addValues(getPropertyConstants()); - if(operand instanceof PCTLProbBoundedUntil) - { - try + try { + + if (operand instanceof PCTLProbNext) + { + int expressionPointer = ((PCTLProbNext)operand).getOperand().toSimulator(this); + return loadPctlNext(expressionPointer); + } + else if (operand instanceof PCTLProbBoundedUntil) { int leftExpressionPointer = ((PCTLProbBoundedUntil)operand).getOperand1().toSimulator(this); int rightExpressionPointer = ((PCTLProbBoundedUntil)operand).getOperand2().toSimulator(this); - + double lowerBound; + if (((PCTLProbBoundedUntil)operand).getLowerBound() != null) + lowerBound = ((PCTLProbBoundedUntil)operand).getLowerBound().evaluateDouble(allConstants, null); + else + lowerBound = 0.0; double upperBound; - - if(((PCTLProbBoundedUntil)operand).getUpperBound() != null) + if (((PCTLProbBoundedUntil)operand).getUpperBound() != null) upperBound = ((PCTLProbBoundedUntil)operand).getUpperBound().evaluateDouble(allConstants, null); else upperBound = Integer.MAX_VALUE; - + return loadPctlBoundedUntil(leftExpressionPointer, rightExpressionPointer, lowerBound, upperBound); + } + else if (operand instanceof PCTLProbUntil) + { + int leftExpressionPointer = ((PCTLProbUntil)operand).getOperand1().toSimulator(this); + int rightExpressionPointer = ((PCTLProbUntil)operand).getOperand2().toSimulator(this); + return loadPctlUntil(leftExpressionPointer, rightExpressionPointer); + } + else if (operand instanceof PCTLProbBoundedFuture) + { + int leftExpressionPointer = (new PCTLExpression(new ExpressionTrue())).toSimulator(this); + int rightExpressionPointer = ((PCTLProbFuture)operand).getOperand().toSimulator(this); double lowerBound; - if(((PCTLProbBoundedUntil)operand).getLowerBound() != null) - lowerBound = ((PCTLProbBoundedUntil)operand).getLowerBound().evaluateDouble(allConstants, null); + if (((PCTLProbBoundedFuture)operand).getLowerBound() != null) + lowerBound = ((PCTLProbBoundedFuture)operand).getLowerBound().evaluateDouble(allConstants, null); else lowerBound = 0.0; - - return loadPctlBoundedUntil(leftExpressionPointer, rightExpressionPointer, lowerBound, upperBound); - + double upperBound; + if (((PCTLProbBoundedFuture)operand).getUpperBound() != null) + upperBound = ((PCTLProbBoundedFuture)operand).getUpperBound().evaluateDouble(allConstants, null); + else + upperBound = Integer.MAX_VALUE; + return loadPctlBoundedUntil(leftExpressionPointer, rightExpressionPointer, lowerBound, upperBound); } - catch(SimulatorException e) + else if (operand instanceof PCTLProbFuture) { - System.err.println("Property: "+operand.toString()+" could not be used in the simulator because: \n"+ e.toString()); - return -1; + int leftExpressionPointer = (new PCTLExpression(new ExpressionTrue())).toSimulator(this); + int rightExpressionPointer = ((PCTLProbFuture)operand).getOperand().toSimulator(this); + return loadPctlUntil(leftExpressionPointer, rightExpressionPointer); } - catch(PrismException e) + else if (operand instanceof PCTLProbBoundedGlobal) { - System.err.println("Property: "+operand.toString()+" could not be used in the simulator because: \n"+ e.toString()); - return -1; + int leftExpressionPointer = (new PCTLExpression(new ExpressionTrue())).toSimulator(this); + int rightExpressionPointer = (new PCTLNot(((PCTLProbGlobal)operand).getOperand())).toSimulator(this); + double lowerBound; + if (((PCTLProbBoundedGlobal)operand).getLowerBound() != null) + lowerBound = ((PCTLProbBoundedGlobal)operand).getLowerBound().evaluateDouble(allConstants, null); + else + lowerBound = 0.0; + double upperBound; + if (((PCTLProbBoundedGlobal)operand).getUpperBound() != null) + upperBound = ((PCTLProbBoundedFuture)operand).getUpperBound().evaluateDouble(allConstants, null); + else + upperBound = Integer.MAX_VALUE; + return loadPctlBoundedUntilNegated(leftExpressionPointer, rightExpressionPointer, lowerBound, upperBound); } - - - } - else if(operand instanceof PCTLProbNext) - { - try + else if (operand instanceof PCTLProbGlobal) { - - int expressionPointer = ((PCTLProbNext)operand).getOperand().toSimulator(this); - - return loadPctlNext(expressionPointer); + int leftExpressionPointer = (new PCTLExpression(new ExpressionTrue())).toSimulator(this); + int rightExpressionPointer = (new PCTLNot(((PCTLProbGlobal)operand).getOperand())).toSimulator(this); + return loadPctlUntilNegated(leftExpressionPointer, rightExpressionPointer); } - catch(SimulatorException e) + else { - System.err.println("Property: "+operand.toString()+" could not be used in the simulator because: \n"+ e.toString()); return -1; } } - else if(operand instanceof PCTLProbUntil) + catch(SimulatorException e) { - try - { - int leftExpressionPointer = ((PCTLProbUntil)operand).getOperand1().toSimulator(this); - int rightExpressionPointer = ((PCTLProbUntil)operand).getOperand2().toSimulator(this); - - return loadPctlUntil(leftExpressionPointer, rightExpressionPointer); - - } - catch(SimulatorException e) - { - System.err.println("Property: "+operand.toString()+" could not be used in the simulator because: \n"+ e.toString()); - return -1; - } + System.err.println("Property: "+operand.toString()+" could not be used in the simulator because: \n"+ e.toString()); + return -1; } - else + catch(PrismException e) { - //System.out.println("cannot be added"); - //cannot be added + System.err.println("Property: "+operand.toString()+" could not be used in the simulator because: \n"+ e.toString()); return -1; } } @@ -2535,8 +2550,10 @@ public class SimulatorEngine //location private static native int loadPctlBoundedUntil(int leftExprPointer, int rightExprPointer, double lowerBound, double upperBound); + private static native int loadPctlBoundedUntilNegated(int leftExprPointer, int rightExprPointer, double lowerBound, double upperBound); private static native int loadPctlUntil(int leftExprPointer, int rightExprPointer); + private static native int loadPctlUntilNegated(int leftExprPointer, int rightExprPointer); private static native int loadPctlNext(int exprPointer); diff --git a/prism/src/simulator/simpctl.cc b/prism/src/simulator/simpctl.cc index 23e026d9..062fe825 100644 --- a/prism/src/simulator/simpctl.cc +++ b/prism/src/simulator/simpctl.cc @@ -79,6 +79,16 @@ CPathFormula::CPathFormula() { answer_known = false; answer = false; + negate = false; +} + + +/* + * Set whether or not the value of this formula should be negated + */ +void CPathFormula::Set_Negate(bool b) +{ + negate = b; } /* @@ -86,7 +96,7 @@ CPathFormula::CPathFormula() */ bool CPathFormula::Get_Answer() { - return answer; + return (negate)?(!answer):(answer); } /* diff --git a/prism/src/simulator/simpctlbuilder.cc b/prism/src/simulator/simpctlbuilder.cc index 0a46bcd7..8609ce31 100644 --- a/prism/src/simulator/simpctlbuilder.cc +++ b/prism/src/simulator/simpctlbuilder.cc @@ -78,6 +78,20 @@ JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_loadPctlBoundedUntil return Formula_To_JInt(bu); } +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_loadPctlBoundedUntilNegated + (JNIEnv *env, jclass cls, jint exprPointer1, jint exprPointer2, jdouble lowerBound, jdouble upperBound, jboolean) +{ + CExpression* expr1 = To_Expr(exprPointer1); + CExpression* expr2 = To_Expr(exprPointer2); + + CBoundedUntil* bu = new CBoundedUntil(expr1, expr2, (double)lowerBound, (double)upperBound); + bu->Set_Negate(true); + + Register_Path_Formula(bu); + + return Formula_To_JInt(bu); +} + /* * Class: simulator_SimulatorEngine * Method: loadPctlUntil @@ -96,6 +110,20 @@ JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_loadPctlUntil return Formula_To_JInt(bu); } +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_loadPctlUntilNegated + (JNIEnv *env, jclass cls, jint exprPointer1, jint exprPointer2) +{ + CExpression* expr1 = To_Expr(exprPointer1); + CExpression* expr2 = To_Expr(exprPointer2); + + CUntil* bu = new CUntil(expr1, expr2); + bu->Set_Negate(true); + + Register_Path_Formula(bu); + + return Formula_To_JInt(bu); +} + /* * Class: simulator_SimulatorEngine * Method: loadPctlNext