diff --git a/prism/include/SimulatorEngine.h b/prism/include/SimulatorEngine.h index 278593e3..32e2b095 100644 --- a/prism/include/SimulatorEngine.h +++ b/prism/include/SimulatorEngine.h @@ -1,1005 +1,1013 @@ /* 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: getCumulativeTimeSpentInPathState - * Signature: (I)D - */ -JNIEXPORT jdouble JNICALL Java_simulator_SimulatorEngine_getCumulativeTimeSpentInPathState - (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: getCumulativeTimeSpentInPathState + * Signature: (I)D + */ +JNIEXPORT jdouble JNICALL Java_simulator_SimulatorEngine_getCumulativeTimeSpentInPathState + (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__IZ (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: doAutomaticChoices + * Signature: (DZ)I + */ +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_doAutomaticChoices__DZ + (JNIEnv *, jclass, jdouble, 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 (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: loadPctlBoundedUntilNegated - * Signature: (IIDD)I - */ -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_loadPctlBoundedUntilNegated + +/* + * 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 + +/* + * 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/simengine.h b/prism/include/simengine.h index 198639b9..c9b3c58a 100644 --- a/prism/include/simengine.h +++ b/prism/include/simengine.h @@ -134,6 +134,9 @@ int Engine_Make_Manual_Update(int index, double time_in_state); int Engine_Do_Automatic_Choices(int n); int Engine_Do_Automatic_Choices(int n, bool detect); +int Engine_Do_Automatic_Choices(double time); +int Engine_Do_Automatic_Choices(double time, bool detect); + int Engine_Do_Backtrack(int step); int Engine_Do_Remove_Preceding_States(int step); diff --git a/prism/include/simpath.h b/prism/include/simpath.h index 0e100e02..dcb1d56e 100644 --- a/prism/include/simpath.h +++ b/prism/include/simpath.h @@ -116,6 +116,12 @@ void Manual_Update(int, double time_in_state); void Automatic_Choices(int n); void Automatic_Choices(int n, bool detect); +/* + * Make automatic updates untill time is passed, and stores the path. + */ +void Automatic_Choices(double time); +void Automatic_Choices(double time, bool detect); + /* * Removes all states following the given index from * the path and sets the state_variables to that state. diff --git a/prism/src/simulator/SimulatorEngine.cc b/prism/src/simulator/SimulatorEngine.cc index 24e21135..ef2e930e 100644 --- a/prism/src/simulator/SimulatorEngine.cc +++ b/prism/src/simulator/SimulatorEngine.cc @@ -363,8 +363,8 @@ JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_makeManualUpdate__ID return 0; } -JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_doAutomaticChoices -(JNIEnv *env, jclass cls, jint n, jboolean detect) +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_doAutomaticChoices__IZ + (JNIEnv *, jclass, jint n, jboolean detect) { try { @@ -378,6 +378,21 @@ JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_doAutomaticChoices return 0; } +JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_doAutomaticChoices__DZ + (JNIEnv *, jclass, jdouble time, jboolean detect) +{ + try + { + Automatic_Choices((double)time, (bool)detect); + } + catch(string str) + { + cout << str << endl; + return simulator_SimulatorEngine_ERROR; + } + return 0; +} + JNIEXPORT jint JNICALL Java_simulator_SimulatorEngine_doBacktrack (JNIEnv *env, jclass cls, jint step) { diff --git a/prism/src/simulator/SimulatorEngine.java b/prism/src/simulator/SimulatorEngine.java index 75eb2059..ebfc22ef 100644 --- a/prism/src/simulator/SimulatorEngine.java +++ b/prism/src/simulator/SimulatorEngine.java @@ -1206,7 +1206,7 @@ public class SimulatorEngine { automaticChoices(n, true); } - + /** * This function makes n automatic choices of updates to the global * state. @@ -1221,11 +1221,41 @@ public class SimulatorEngine throw new SimulatorException(getLastErrorMessage()); } + /** + * This function makes a number of automatic choices of updates to the global + * state, untill `time' has passed. + * @param time is the length of time to pass. + * @throws SimulatorException if something goes wrong when updating the state. + */ + public void automaticChoices(double time) throws SimulatorException + { + automaticChoices(time, true); + } + + /** + * This function makes n automatic choices of updates to the global + * state, untill `time' has passed. + * @param time is the length of time to pass. + * @param detect whether to employ loop detection. + * @throws SimulatorException if something goes wrong when updating the state. + */ + public void automaticChoices(double time, boolean detect) throws SimulatorException + { + int result = doAutomaticChoices(time, detect); + if(result == ERROR) + throw new SimulatorException(getLastErrorMessage()); + } + /** * Ask c++ engine to make n automatic updates to the global state. */ private static native int doAutomaticChoices(int n, boolean detect); + /** + * Ask c++ engine to make some automatic updates to the global state, up to some time. + */ + private static native int doAutomaticChoices(double time, boolean detect); + /** * This function backtracks the current path to the state of the * given index diff --git a/prism/src/simulator/simengine.cc b/prism/src/simulator/simengine.cc index 94809af7..6d1d0d8a 100644 --- a/prism/src/simulator/simengine.cc +++ b/prism/src/simulator/simengine.cc @@ -360,6 +360,24 @@ int Engine_Do_Automatic_Choices(int n, bool detect) return 0; } +int Engine_Do_Automatic_Choices(double time) +{ + return Engine_Do_Automatic_Choices(time, true); +} + +int Engine_Do_Automatic_Choices(double time, bool detect) +{ + try + { + Automatic_Choices(time, detect); + } + catch(char* str) + { + return ERROR; + } + return 0; +} + int Engine_Do_Backtrack(int step) { try diff --git a/prism/src/simulator/simpath.cc b/prism/src/simulator/simpath.cc index 0c2319d8..9cab740f 100644 --- a/prism/src/simulator/simpath.cc +++ b/prism/src/simulator/simpath.cc @@ -385,6 +385,71 @@ void Automatic_Choices(int n, bool detect) } } +/* +* Make choices untill time has passed and update the path. +*/ +void Automatic_Choices(double time){ Automatic_Choices(time, true); } + +void Automatic_Choices(double time, bool detect) +{ + if (model_type != STOCHASTIC) + Automatic_Choices((int)ceil(time), detect); + else + { + double startTime = path_timer; + double currentTime = startTime; + + while (currentTime - startTime < time) + { + /* Break when looping. */ + if (detect && loop_detection->Is_Proven_Looping()) + break; + + /* Break when deadlocking. */ + if (loop_detection->Is_Deadlock()) + break; + + double probability = 0.0; + Automatic_Update(loop_detection, probability); + + // Because we cannot guarantee that we know the selected index, we have to show this. + stored_path[current_index]->choice_made = PATH_NO_CHOICE_MADE; + stored_path[current_index]->probability = probability; + + // Unless requested not to (detect==false), this function will stop exploring when a loop is detected. + // Because Automatic_Update() checks for loops before making a transition, we overshoot. + // Hence at this point if we are looping we step back a state, + // i.e. reset state_variables and don't add new state to the path. + + if (detect && loop_detection->Is_Proven_Looping()) + { + stored_path[current_index]->Make_Current_State_This(); + } + else + { + // Add state to path (unless we have stayed in the same state because of deadlock). + if (!loop_detection->Is_Deadlock()) + Add_Current_State_To_Path(); + currentTime = path_timer; + } + + Calculate_State_Reward(state_variables); + } + + Calculate_Updates(state_variables); + + // check for looping + if(Are_Updates_Deterministic()) + { + loop_detection->Notify_Deterministic_State(false); + } + else + { + loop_detection->Notify_Deterministic_Path_End(); + } + } +} + /* * Removes all states following the given index from * the path and sets the state_variables to that state. diff --git a/prism/src/userinterface/simulator/GUISimulator.java b/prism/src/userinterface/simulator/GUISimulator.java index 90497e81..f292baeb 100644 --- a/prism/src/userinterface/simulator/GUISimulator.java +++ b/prism/src/userinterface/simulator/GUISimulator.java @@ -292,11 +292,11 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect typeExploreCombo.addItem("Steps"); typeExploreCombo.addItem("Up to step"); - /*if (mf != null && mf.getType() == ModulesFile.STOCHASTIC) + if (mf != null && mf.getType() == ModulesFile.STOCHASTIC) { typeExploreCombo.addItem("Time"); typeExploreCombo.addItem("Up to time"); - }*/ + } typeBacktrackCombo.setEnabled(pathActive); typeBacktrackCombo.removeAllItems(); @@ -453,7 +453,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect } } - /** Backtracks a number of steps. */ + /** Explore a number of steps. */ public void a_autoStep(int noSteps) { try @@ -494,6 +494,49 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect } } + /** Explore an amount of time. */ + public void a_autoStep(double time) + { + try + { + if (displayPathLoops && pathTableModel.isPathLooping()) + { + if (questionYesNo("A loop in the path has been detected. Do you wish to disable loop detection and extend the path?") == 0) + { + displayPathLoops = false; + pathTable.repaint(); + } + else return; + } + + setComputing(true); + + if(isOldUpdate()) + { + engine.finishedWithOldUpdates(); + } + + engine.automaticChoices(time, displayPathLoops); + + pathTableModel.updatePathTable(); + updateTableModel.updateUpdatesTable(); + pathTable.scrollRectToVisible(new Rectangle(0, (int)pathTable.getPreferredSize().getHeight() - 10, (int)pathTable.getPreferredSize().getWidth(), (int)pathTable.getPreferredSize().getHeight()) ); + + totalTimeLabel.setText(PrismUtils.formatDouble(this.getPrism().getSettings(), engine.getTotalPathTime())); + pathLengthLabel.setText(""+(engine.getPathSize()-1)); + + stateLabelList.repaint(); + pathFormulaeList.repaint(); + setComputing(false); + } + catch(SimulatorException e) + { + this.error(e.getMessage()); + } + } + + + /** Backtracks to a certain step. */ public void a_backTrack(int step) throws SimulatorException { @@ -1549,65 +1592,109 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect a_restartPath(); }//GEN-LAST:event_resetPathButtonActionPerformed - private void inputExploreFieldActionPerformed(java.awt.event.ActionEvent evt) {//GEN-FIRST:event_inputExploreFieldActionPerformed - - }//GEN-LAST:event_inputExploreFieldActionPerformed + private void inputExploreFieldActionPerformed(java.awt.event.ActionEvent evt) {//GEN-FIRST:event_inputExploreFieldActionPerformed - private void randomExplorationButtonActionPerformed(java.awt.event.ActionEvent evt) {//GEN-FIRST:event_randomExplorationButtonActionPerformed + }//GEN-LAST:event_inputExploreFieldActionPerformed + + private void randomExplorationButtonActionPerformed(java.awt.event.ActionEvent evt) {//GEN-FIRST:event_randomExplorationButtonActionPerformed - try - { - /* Update some given number of steps. */ - if (typeExploreCombo.getSelectedIndex() == 0) + try + { + /* Update some given number of steps. */ + if (typeExploreCombo.getSelectedIndex() == 0) + { + int noSteps = 1; + + try { - int noSteps = 1; + if (inputExploreField.getText().trim().length() == 0) + throw new NumberFormatException(); - try - { - if (inputExploreField.getText().trim().length() == 0) - throw new SimulatorException("The \"Num. steps\" parameter is invalid.\nIt must be a positive integer, but it is currently empty"); - - noSteps = Integer.parseInt(inputExploreField.getText().trim()); - - if (noSteps <= 0) - throw new SimulatorException("The \"Num. steps\" parameter is invalid.\nIt must be a positive integer"); - - a_autoStep(noSteps); - } - catch (NumberFormatException nfe) - { - throw new SimulatorException("The \"Num. steps\" parameter is invalid.\nThe current input (\""+inputExploreField.getText().trim()+"\") is not a valid positive integer"); - } + noSteps = Integer.parseInt(inputExploreField.getText().trim()); + + if (noSteps <= 0) + throw new NumberFormatException(); + + a_autoStep(noSteps); } - /* Update upto some state. */ - else if (typeExploreCombo.getSelectedIndex() == 1) + catch (NumberFormatException nfe) { - int uptoState; + throw new SimulatorException("The \"Steps\" parameter is invalid, it must be a positive integer."); + } + } + /* Update upto some state. */ + else if (typeExploreCombo.getSelectedIndex() == 1) + { + int uptoState; + + try + { + if (inputExploreField.getText().trim().length() == 0) + throw new NumberFormatException(); - try - { - if (inputExploreField.getText().trim().length() == 0) - throw new SimulatorException("The \"To state\" parameter is invalid.\nIt must be a positive integer larger than the index of the current state ("+(engine.getPathSize()-1)+"), but it is currently empty"); - - uptoState = Integer.parseInt(inputExploreField.getText().trim()); - - if (uptoState < engine.getPathSize()) - throw new SimulatorException("The \"To state\" parameter is invalid.\nIt must be a positive integer larger than the index of the current state ("+(engine.getPathSize()-1)+")"); - - a_autoStep(uptoState - engine.getPathSize() + 1); - } - catch (NumberFormatException nfe) - { - throw new SimulatorException("The \"To state\" parameter is invalid.\nThe current input (\""+inputExploreField.getText().trim()+"\") is not a valid positive integer"); - } + uptoState = Integer.parseInt(inputExploreField.getText().trim()); + + if (uptoState < engine.getPathSize()) + throw new NumberFormatException(); + + a_autoStep(uptoState - engine.getPathSize() + 1); } - } - catch (SimulatorException se) - { - this.error(se.getMessage()); - } - }//GEN-LAST:event_randomExplorationButtonActionPerformed - + catch (NumberFormatException nfe) + { + throw new SimulatorException("The \"Up to state\" parameter is invalid, it must be a positive integer larger than the index of the current state (which is "+ (engine.getPathSize()-1)+")"); + } + } + else if (typeExploreCombo.getSelectedIndex() == 2) + { + double time; + + try + { + if (inputExploreField.getText().trim().length() == 0) + throw new NumberFormatException(); + + time = Double.parseDouble(inputExploreField.getText().trim()); + + if (time < 0.0d) + throw new NumberFormatException(); + + a_autoStep(time); + } + catch (NumberFormatException nfe) + { + throw new SimulatorException("The \"Time\" parameter is invalid, it must be a positive double"); + } + } + else if (typeExploreCombo.getSelectedIndex() == 3) + { + double time; + double currentTime = engine.getTotalPathTime(); + + try + { + if (inputExploreField.getText().trim().length() == 0) + throw new NumberFormatException(); + + time = Double.parseDouble(inputExploreField.getText().trim()); + + if (time <= currentTime) + throw new NumberFormatException(); + + a_autoStep(time-currentTime); + } + catch (NumberFormatException nfe) + { + throw new SimulatorException("The \"Time\" parameter is invalid, it must be a positive double larger than the cumulative path time (which is currently " + currentTime+")"); + } + } + + } + catch (SimulatorException se) + { + this.error(se.getMessage()); + } + }//GEN-LAST:event_randomExplorationButtonActionPerformed + private void newPathButtonActionPerformed(java.awt.event.ActionEvent evt)//GEN-FIRST:event_newPathButtonActionPerformed {//GEN-HEADEREND:event_newPathButtonActionPerformed a_newPath();