===== Physical Design =====
Used states:
* init0: [enteredPin, 1111],[correctPin, 1111],[desiredAmount, 100.0],[cashPointAmount, 100000.0],[userAccountAmount, 10000.0],[userRequestedAction, withdraw]
* init1: [enteredPin, 1111],[correctPin, 1112],[desiredAmount, 100.0],[cashPointAmount, 100000.0],[userAccountAmount, 10000.0],[userRequestedAction, withdraw]
* init2: [enteredPin, 1111],[correctPin, 1111],[desiredAmount, 100.0],[cashPointAmount, 10.0],[userAccountAmount, 10000.0],[userRequestedAction, withdraw]
* init3: [enteredPin, 1111],[correctPin, 1111],[desiredAmount, 100.0],[cashPointAmount, 1000.0],[userAccountAmount, 10.0],[userRequestedAction, withdraw]
==== Trajectory 1 ====
From state ''init0'' using ''ddi'' inference mode
TRAJECTROY: Rule start has generated state: [[enteredPin, 1111], [correctPin, 1111], [desiredAmount, 100.0], [cashPointAmount, 100000.0], [userAccountAmount, 10000.0], [userRequestedAction, withdraw]]
TRAJECTROY: Rule Table3/1 has generated state: [[enteredPin, 1111], [correctPin, 1111], [desiredAmount, 100.0], [cashPointAmount, 100000.0], [userAccountAmount, 10000.0], [userRequestedAction, withdraw], [pinDifference, 0]]
TRAJECTROY: Rule Table2/1 has generated state: [[enteredPin, 1111], [correctPin, 1111], [desiredAmount, 100.0], [cashPointAmount, 100000.0], [userAccountAmount, 10000.0], [userRequestedAction, withdraw], [pinDifference, 0], [authorizated, false], [failedAttempts, 3]]
TRAJECTROY: Rule Table2/2 has generated state: [[enteredPin, 1111], [correctPin, 1111], [desiredAmount, 100.0], [cashPointAmount, 100000.0], [userAccountAmount, 10000.0], [userRequestedAction, withdraw], [pinDifference, 0], [authorizated, true], [failedAttempts, 2]]
TRAJECTROY: Rule Table5/1 has generated state: [[enteredPin, 1111], [correctPin, 1111], [desiredAmount, 100.0], [cashPointAmount, 100000.0], [userAccountAmount, 10000.0], [userRequestedAction, withdraw], [pinDifference, 0], [authorizated, true], [failedAttempts, 2], [cdAmountDifference, 99900.0]]
TRAJECTROY: Rule Table4/1 has generated state: [[enteredPin, 1111], [correctPin, 1111], [desiredAmount, 100.0], [cashPointAmount, 100000.0], [userAccountAmount, 10000.0], [userRequestedAction, withdraw], [pinDifference, 0], [authorizated, true], [failedAttempts, 2], [cdAmountDifference, 99900.0], [udAmountDifference, 9900.0]]
TRAJECTROY: Rule Table1/4 has generated state: [[enteredPin, 1111], [correctPin, 1111], [desiredAmount, 100.0], [cashPointAmount, 100000.0], [userAccountAmount, 10000.0], [userRequestedAction, withdraw], [pinDifference, 0], [authorizated, true], [failedAttempts, 2], [cdAmountDifference, 99900.0], [udAmountDifference, 9900.0], [cashPointActivity, payOut]]
==== Trajectory 2 ====
From state ''init1'' using ''ddi'' inference mode
TRAJECTROY: Rule start has generated state: [[enteredPin, 1111], [correctPin, 1112], [desiredAmount, 100.0], [cashPointAmount, 100000.0], [userAccountAmount, 10000.0], [userRequestedAction, withdraw]]
TRAJECTROY: Rule Table3/1 has generated state: [[enteredPin, 1111], [correctPin, 1112], [desiredAmount, 100.0], [cashPointAmount, 100000.0], [userAccountAmount, 10000.0], [userRequestedAction, withdraw], [pinDifference, 0]]
TRAJECTROY: Rule Table2/1 has generated state: [[enteredPin, 1111], [correctPin, 1112], [desiredAmount, 100.0], [cashPointAmount, 100000.0], [userAccountAmount, 10000.0], [userRequestedAction, withdraw], [pinDifference, 0], [authorizated, false], [failedAttempts, 3]]
TRAJECTROY: Rule Table2/2 has generated state: [[enteredPin, 1111], [correctPin, 1112], [desiredAmount, 100.0], [cashPointAmount, 100000.0], [userAccountAmount, 10000.0], [userRequestedAction, withdraw], [pinDifference, 0], [authorizated, true], [failedAttempts, 2]]
TRAJECTROY: Rule Table5/1 has generated state: [[enteredPin, 1111], [correctPin, 1112], [desiredAmount, 100.0], [cashPointAmount, 100000.0], [userAccountAmount, 10000.0], [userRequestedAction, withdraw], [pinDifference, 0], [authorizated, true], [failedAttempts, 2], [cdAmountDifference, 99900.0]]
TRAJECTROY: Rule Table4/1 has generated state: [[enteredPin, 1111], [correctPin, 1112], [desiredAmount, 100.0], [cashPointAmount, 100000.0], [userAccountAmount, 10000.0], [userRequestedAction, withdraw], [pinDifference, 0], [authorizated, true], [failedAttempts, 2], [cdAmountDifference, 99900.0], [udAmountDifference, 9900.0]]
TRAJECTROY: Rule Table1/4 has generated state: [[enteredPin, 1111], [correctPin, 1112], [desiredAmount, 100.0], [cashPointAmount, 100000.0], [userAccountAmount, 10000.0], [userRequestedAction, withdraw], [pinDifference, 0], [authorizated, true], [failedAttempts, 2], [cdAmountDifference, 99900.0], [udAmountDifference, 9900.0], [cashPointActivity, payOut]]
==== Trajectory 3 ====
From state ''init2'' using ''ddi'' inference mode
TRAJECTROY: Rule start has generated state: [[enteredPin, 1111], [correctPin, 1111], [desiredAmount, 100.0], [cashPointAmount, 10.0], [userAccountAmount, 10000.0], [userRequestedAction, withdraw]]
TRAJECTROY: Rule Table3/1 has generated state: [[enteredPin, 1111], [correctPin, 1111], [desiredAmount, 100.0], [cashPointAmount, 10.0], [userAccountAmount, 10000.0], [userRequestedAction, withdraw], [pinDifference, 0]]
TRAJECTROY: Rule Table2/1 has generated state: [[enteredPin, 1111], [correctPin, 1111], [desiredAmount, 100.0], [cashPointAmount, 10.0], [userAccountAmount, 10000.0], [userRequestedAction, withdraw], [pinDifference, 0], [authorizated, false], [failedAttempts, 3]]
TRAJECTROY: Rule Table2/2 has generated state: [[enteredPin, 1111], [correctPin, 1111], [desiredAmount, 100.0], [cashPointAmount, 10.0], [userAccountAmount, 10000.0], [userRequestedAction, withdraw], [pinDifference, 0], [authorizated, true], [failedAttempts, 2]]
TRAJECTROY: Rule Table5/1 has generated state: [[enteredPin, 1111], [correctPin, 1111], [desiredAmount, 100.0], [cashPointAmount, 10.0], [userAccountAmount, 10000.0], [userRequestedAction, withdraw], [pinDifference, 0], [authorizated, true], [failedAttempts, 2], [cdAmountDifference, 99900.0]]
TRAJECTROY: Rule Table4/1 has generated state: [[enteredPin, 1111], [correctPin, 1111], [desiredAmount, 100.0], [cashPointAmount, 10.0], [userAccountAmount, 10000.0], [userRequestedAction, withdraw], [pinDifference, 0], [authorizated, true], [failedAttempts, 2], [cdAmountDifference, 99900.0], [udAmountDifference, 9900.0]]
TRAJECTROY: Rule Table1/4 has generated state: [[enteredPin, 1111], [correctPin, 1111], [desiredAmount, 100.0], [cashPointAmount, 10.0], [userAccountAmount, 10000.0], [userRequestedAction, withdraw], [pinDifference, 0], [authorizated, true], [failedAttempts, 2], [cdAmountDifference, 99900.0], [udAmountDifference, 9900.0], [cashPointActivity, payOut]]
==== Trajectory 4 ====
From state ''init3'' using ''ddi'' inference mode
TRAJECTROY: Rule start has generated state: [[enteredPin, 1111], [correctPin, 1111], [desiredAmount, 100.0], [cashPointAmount, 1000.0], [userAccountAmount, 10.0], [userRequestedAction, withdraw]]
TRAJECTROY: Rule Table3/1 has generated state: [[enteredPin, 1111], [correctPin, 1111], [desiredAmount, 100.0], [cashPointAmount, 1000.0], [userAccountAmount, 10.0], [userRequestedAction, withdraw], [pinDifference, 0]]
TRAJECTROY: Rule Table2/1 has generated state: [[enteredPin, 1111], [correctPin, 1111], [desiredAmount, 100.0], [cashPointAmount, 1000.0], [userAccountAmount, 10.0], [userRequestedAction, withdraw], [pinDifference, 0], [authorizated, false], [failedAttempts, 3]]
TRAJECTROY: Rule Table2/2 has generated state: [[enteredPin, 1111], [correctPin, 1111], [desiredAmount, 100.0], [cashPointAmount, 1000.0], [userAccountAmount, 10.0], [userRequestedAction, withdraw], [pinDifference, 0], [authorizated, true], [failedAttempts, 2]]
TRAJECTROY: Rule Table5/1 has generated state: [[enteredPin, 1111], [correctPin, 1111], [desiredAmount, 100.0], [cashPointAmount, 1000.0], [userAccountAmount, 10.0], [userRequestedAction, withdraw], [pinDifference, 0], [authorizated, true], [failedAttempts, 2], [cdAmountDifference, 99900.0]]
TRAJECTROY: Rule Table4/1 has generated state: [[enteredPin, 1111], [correctPin, 1111], [desiredAmount, 100.0], [cashPointAmount, 1000.0], [userAccountAmount, 10.0], [userRequestedAction, withdraw], [pinDifference, 0], [authorizated, true], [failedAttempts, 2], [cdAmountDifference, 99900.0], [udAmountDifference, 9900.0]]
TRAJECTROY: Rule Table1/4 has generated state: [[enteredPin, 1111], [correctPin, 1111], [desiredAmount, 100.0], [cashPointAmount, 1000.0], [userAccountAmount, 10.0], [userRequestedAction, withdraw], [pinDifference, 0], [authorizated, true], [failedAttempts, 2], [cdAmountDifference, 99900.0], [udAmountDifference, 9900.0], [cashPointActivity, payOut]]
==== Trajectory 5 ====
From state ''init0'' using ''gdi'' inference mode
TRAJECTROY: Rule start has generated state: [[enteredPin, 1111], [correctPin, 1111], [desiredAmount, 100.0], [cashPointAmount, 100000.0], [userAccountAmount, 10000.0], [userRequestedAction, withdraw]]
TRAJECTROY: Rule Table3/1 has generated state: [[enteredPin, 1111], [correctPin, 1111], [desiredAmount, 100.0], [cashPointAmount, 100000.0], [userAccountAmount, 10000.0], [userRequestedAction, withdraw], [pinDifference, 0]]
TRAJECTROY: Rule Table2/1 has generated state: [[enteredPin, 1111], [correctPin, 1111], [desiredAmount, 100.0], [cashPointAmount, 100000.0], [userAccountAmount, 10000.0], [userRequestedAction, withdraw], [pinDifference, 0], [authorizated, false], [failedAttempts, 3]]
TRAJECTROY: Rule Table2/2 has generated state: [[enteredPin, 1111], [correctPin, 1111], [desiredAmount, 100.0], [cashPointAmount, 100000.0], [userAccountAmount, 10000.0], [userRequestedAction, withdraw], [pinDifference, 0], [authorizated, true], [failedAttempts, 2]]
TRAJECTROY: Rule Table4/1 has generated state: [[enteredPin, 1111], [correctPin, 1111], [desiredAmount, 100.0], [cashPointAmount, 100000.0], [userAccountAmount, 10000.0], [userRequestedAction, withdraw], [pinDifference, 0], [authorizated, true], [failedAttempts, 2], [udAmountDifference, 9900.0]]
TRAJECTROY: Rule Table5/1 has generated state: [[enteredPin, 1111], [correctPin, 1111], [desiredAmount, 100.0], [cashPointAmount, 100000.0], [userAccountAmount, 10000.0], [userRequestedAction, withdraw], [pinDifference, 0], [authorizated, true], [failedAttempts, 2], [udAmountDifference, 9900.0], [cdAmountDifference, 99900.0]]
TRAJECTROY: Rule Table1/4 has generated state: [[enteredPin, 1111], [correctPin, 1111], [desiredAmount, 100.0], [cashPointAmount, 100000.0], [userAccountAmount, 10000.0], [userRequestedAction, withdraw], [pinDifference, 0], [authorizated, true], [failedAttempts, 2], [udAmountDifference, 9900.0], [cdAmountDifference, 99900.0], [cashPointActivity, payOut]]
==== Trajectory 6 ====
From state ''init1'' using ''gdi'' inference mode
TRAJECTROY: Rule start has generated state: [[enteredPin, 1111], [correctPin, 1112], [desiredAmount, 100.0], [cashPointAmount, 100000.0], [userAccountAmount, 10000.0], [userRequestedAction, withdraw]]
TRAJECTROY: Rule Table3/1 has generated state: [[enteredPin, 1111], [correctPin, 1112], [desiredAmount, 100.0], [cashPointAmount, 100000.0], [userAccountAmount, 10000.0], [userRequestedAction, withdraw], [pinDifference, 0]]
TRAJECTROY: Rule Table2/1 has generated state: [[enteredPin, 1111], [correctPin, 1112], [desiredAmount, 100.0], [cashPointAmount, 100000.0], [userAccountAmount, 10000.0], [userRequestedAction, withdraw], [pinDifference, 0], [authorizated, false], [failedAttempts, 3]]
TRAJECTROY: Rule Table2/2 has generated state: [[enteredPin, 1111], [correctPin, 1112], [desiredAmount, 100.0], [cashPointAmount, 100000.0], [userAccountAmount, 10000.0], [userRequestedAction, withdraw], [pinDifference, 0], [authorizated, true], [failedAttempts, 2]]
TRAJECTROY: Rule Table4/1 has generated state: [[enteredPin, 1111], [correctPin, 1112], [desiredAmount, 100.0], [cashPointAmount, 100000.0], [userAccountAmount, 10000.0], [userRequestedAction, withdraw], [pinDifference, 0], [authorizated, true], [failedAttempts, 2], [udAmountDifference, 9900.0]]
TRAJECTROY: Rule Table5/1 has generated state: [[enteredPin, 1111], [correctPin, 1112], [desiredAmount, 100.0], [cashPointAmount, 100000.0], [userAccountAmount, 10000.0], [userRequestedAction, withdraw], [pinDifference, 0], [authorizated, true], [failedAttempts, 2], [udAmountDifference, 9900.0], [cdAmountDifference, 99900.0]]
TRAJECTROY: Rule Table1/4 has generated state: [[enteredPin, 1111], [correctPin, 1112], [desiredAmount, 100.0], [cashPointAmount, 100000.0], [userAccountAmount, 10000.0], [userRequestedAction, withdraw], [pinDifference, 0], [authorizated, true], [failedAttempts, 2], [udAmountDifference, 9900.0], [cdAmountDifference, 99900.0], [cashPointActivity, payOut]]
==== Trajectory 7 ====
From state ''init2'' using ''gdi'' inference mode
TRAJECTROY: Rule start has generated state: [[enteredPin, 1111], [correctPin, 1111], [desiredAmount, 100.0], [cashPointAmount, 10.0], [userAccountAmount, 10000.0], [userRequestedAction, withdraw]]
TRAJECTROY: Rule Table3/1 has generated state: [[enteredPin, 1111], [correctPin, 1111], [desiredAmount, 100.0], [cashPointAmount, 10.0], [userAccountAmount, 10000.0], [userRequestedAction, withdraw], [pinDifference, 0]]
TRAJECTROY: Rule Table2/1 has generated state: [[enteredPin, 1111], [correctPin, 1111], [desiredAmount, 100.0], [cashPointAmount, 10.0], [userAccountAmount, 10000.0], [userRequestedAction, withdraw], [pinDifference, 0], [authorizated, false], [failedAttempts, 3]]
TRAJECTROY: Rule Table2/2 has generated state: [[enteredPin, 1111], [correctPin, 1111], [desiredAmount, 100.0], [cashPointAmount, 10.0], [userAccountAmount, 10000.0], [userRequestedAction, withdraw], [pinDifference, 0], [authorizated, true], [failedAttempts, 2]]
TRAJECTROY: Rule Table4/1 has generated state: [[enteredPin, 1111], [correctPin, 1111], [desiredAmount, 100.0], [cashPointAmount, 10.0], [userAccountAmount, 10000.0], [userRequestedAction, withdraw], [pinDifference, 0], [authorizated, true], [failedAttempts, 2], [udAmountDifference, 9900.0]]
TRAJECTROY: Rule Table5/1 has generated state: [[enteredPin, 1111], [correctPin, 1111], [desiredAmount, 100.0], [cashPointAmount, 10.0], [userAccountAmount, 10000.0], [userRequestedAction, withdraw], [pinDifference, 0], [authorizated, true], [failedAttempts, 2], [udAmountDifference, 9900.0], [cdAmountDifference, 99900.0]]
TRAJECTROY: Rule Table1/4 has generated state: [[enteredPin, 1111], [correctPin, 1111], [desiredAmount, 100.0], [cashPointAmount, 10.0], [userAccountAmount, 10000.0], [userRequestedAction, withdraw], [pinDifference, 0], [authorizated, true], [failedAttempts, 2], [udAmountDifference, 9900.0], [cdAmountDifference, 99900.0], [cashPointActivity, payOut]]
==== Trajectory 8 ====
From state ''init3'' using ''gdi'' inference mode
TRAJECTROY: Rule start has generated state: [[enteredPin, 1111], [correctPin, 1111], [desiredAmount, 100.0], [cashPointAmount, 1000.0], [userAccountAmount, 10.0], [userRequestedAction, withdraw]]
TRAJECTROY: Rule Table3/1 has generated state: [[enteredPin, 1111], [correctPin, 1111], [desiredAmount, 100.0], [cashPointAmount, 1000.0], [userAccountAmount, 10.0], [userRequestedAction, withdraw], [pinDifference, 0]]
TRAJECTROY: Rule Table2/1 has generated state: [[enteredPin, 1111], [correctPin, 1111], [desiredAmount, 100.0], [cashPointAmount, 1000.0], [userAccountAmount, 10.0], [userRequestedAction, withdraw], [pinDifference, 0], [authorizated, false], [failedAttempts, 3]]
TRAJECTROY: Rule Table2/2 has generated state: [[enteredPin, 1111], [correctPin, 1111], [desiredAmount, 100.0], [cashPointAmount, 1000.0], [userAccountAmount, 10.0], [userRequestedAction, withdraw], [pinDifference, 0], [authorizated, true], [failedAttempts, 2]]
TRAJECTROY: Rule Table4/1 has generated state: [[enteredPin, 1111], [correctPin, 1111], [desiredAmount, 100.0], [cashPointAmount, 1000.0], [userAccountAmount, 10.0], [userRequestedAction, withdraw], [pinDifference, 0], [authorizated, true], [failedAttempts, 2], [udAmountDifference, 9900.0]]
TRAJECTROY: Rule Table5/1 has generated state: [[enteredPin, 1111], [correctPin, 1111], [desiredAmount, 100.0], [cashPointAmount, 1000.0], [userAccountAmount, 10.0], [userRequestedAction, withdraw], [pinDifference, 0], [authorizated, true], [failedAttempts, 2], [udAmountDifference, 9900.0], [cdAmountDifference, 99900.0]]
TRAJECTROY: Rule Table1/4 has generated state: [[enteredPin, 1111], [correctPin, 1111], [desiredAmount, 100.0], [cashPointAmount, 1000.0], [userAccountAmount, 10.0], [userRequestedAction, withdraw], [pinDifference, 0], [authorizated, true], [failedAttempts, 2], [udAmountDifference, 9900.0], [cdAmountDifference, 99900.0], [cashPointActivity, payOut]]