Add parametric test case

Author: Aishwarya Jagarapu

Tutorial/2_TwoPhaseCommit/PTst/TestDriver.p

@@ -99,3 +99,26 @@ machine MultipleClientsWithFailure {
     }
   }
 }
+
+
+// Test parameters
+param pNumClients: int;
+param pNumParticipants: int;
+param pNumTransPerClient: int;
+param pNumFailures: int;
+
+machine TestWithConfig {
+  start state Init {
+    entry {
+      var config: t2PCConfig;
+      config = (
+        numClients = pNumClients,
+        numParticipants = pNumParticipants,
+        numTransPerClient = pNumTransPerClient,
+        failParticipants = pNumFailures
+      );
+      SetUpTwoPhaseCommitSystem(config);
+    }
+  }
+}
+

Tutorial/2_TwoPhaseCommit/PTst/TestScripts.p

@@ -9,4 +9,13 @@ test tcMultipleClientsNoFailure [main = MultipleClientsNoFailure]:
 
 // asserts the liveness monitor along with the default properties
 test tcMultipleClientsWithFailure [main = MultipleClientsWithFailure]:
-  assert Progress in (union TwoPhaseCommit, TwoPCClient, FailureInjector, { MultipleClientsWithFailure });
+  assert Progress in (union TwoPhaseCommit, TwoPCClient, FailureInjector, { MultipleClientsWithFailure });
+
+
+test param (
+    pNumClients in [2,3],
+    pNumParticipants in [4,6],
+    pNumTransPerClient in [1,2],
+    pNumFailures in [0,1]
+  )  tcParameterizedTwoPhaseCommit [main=TestWithConfig]:
+  assert AtomicityInvariant, Progress in (union TwoPhaseCommit, TwoPCClient, FailureInjector, { TestWithConfig });