diff --git a/ConcurrentPercolator/Test1.tla b/ConcurrentPercolator/Test1.tla index 3f8e7ab..1c320eb 100644 --- a/ConcurrentPercolator/Test1.tla +++ b/ConcurrentPercolator/Test1.tla @@ -1,6 +1,6 @@ --------------------------------- MODULE Test1 --------------------------------- -EXTENDS Percolator, TLC +EXTENDS ConcurrentPercolator, TLC \* We use one table with 3 keys and 3 concurrent clients for TLC model checking. \* These 3 clients have the same primary key, so they are considered symmetric. diff --git a/ConcurrentPercolator/Test2.tla b/ConcurrentPercolator/Test2.tla index 944a649..1537cc8 100644 --- a/ConcurrentPercolator/Test2.tla +++ b/ConcurrentPercolator/Test2.tla @@ -1,6 +1,6 @@ --------------------------------- MODULE Test2 --------------------------------- -EXTENDS Percolator, TLC +EXTENDS ConcurrentPercolator, TLC \* We use one table with 2 keys and 2 concurrent clients for TLC model checking. \* These 2 clients have primary key 1 and 2 respectively.