===== Physical Design =====

Used states:
  * init0: <code>[enteredPin, 1111],[correctPin, 1111],[desiredAmount, 100.0],[cashPointAmount, 100000.0],[userAccountAmount, 10000.0],[userRequestedAction, withdraw]</code>
  * init1: <code>[enteredPin, 1111],[correctPin, 1112],[desiredAmount, 100.0],[cashPointAmount, 100000.0],[userAccountAmount, 10000.0],[userRequestedAction, withdraw]</code> 
  * init2: <code>[enteredPin, 1111],[correctPin, 1111],[desiredAmount, 100.0],[cashPointAmount, 10.0],[userAccountAmount, 10000.0],[userRequestedAction, withdraw]</code>
  * init3: <code>[enteredPin, 1111],[correctPin, 1111],[desiredAmount, 100.0],[cashPointAmount, 1000.0],[userAccountAmount, 10.0],[userRequestedAction, withdraw]</code>


==== Trajectory 1 ====
From state ''init0'' using ''ddi'' inference mode
<code>
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]]
</code>

==== Trajectory 2 ====
From state ''init1'' using ''ddi'' inference mode
<code>
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]]
</code>

==== Trajectory 3 ====
From state ''init2'' using ''ddi'' inference mode
<code>
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]]
</code>

==== Trajectory 4 ====
From state ''init3'' using ''ddi'' inference mode
<code>
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]]
</code>

==== Trajectory 5 ====
From state ''init0'' using ''gdi'' inference mode
<code>
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]]
</code>

==== Trajectory 6 ====
From state ''init1'' using ''gdi'' inference mode
<code>
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]]
</code>

==== Trajectory 7 ====
From state ''init2'' using ''gdi'' inference mode
<code>
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]]
</code>

==== Trajectory 8 ====
From state ''init3'' using ''gdi'' inference mode
<code>
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]]
</code>