Some cleanup

cwi-swat · Oct 27, 2020 · 92d3f37 · 92d3f37
1 parent 44761da
commit 92d3f37
Show file tree

Hide file tree

Showing 6 changed files with 11 additions and 132 deletions.
diff --git a/examples/paper/example/Person.rebel b/examples/paper/example/Person.rebel
diff --git a/examples/paper/example/Transaction.rebel b/examples/paper/example/Transaction.rebel
@@ -19,7 +19,7 @@ spec Transaction
 
   states:
     (*) -> created: create;
-    created -> (*): book;//, fail;
+    created -> (*): book, fail;
 
 spec SimpleAccount
   balance: Integer;
@@ -32,13 +32,13 @@ spec SimpleAccount
     pre: amount > 0;
     post: this.balance' = this.balance + amount;
 
-  assume PositiveBalance = always forall a:SimpleAccount | (a is initialized => a.balance >= 0);
+  assume PositiveBalance = always forall a:SimpleAccount | a.balance >= 0;
 
   states:
     opened -> opened: withdraw, deposit;
 
 //config BasicTrans = t: Transaction is uninitialized, ac1,ac2: Account is uninitialized, an1,an2: AccountNumber, d1:Date, d2:Date;
-config SimplifiedTrans = t: Transaction is uninitialized, ac1,ac2: SimpleAccount abstracts Account;
+config SimplifiedTrans = t: Transaction is uninitialized, ac1,ac2: SimpleAccount mocks Account;
 
 assert CanBookATransaction = eventually exists t: Transaction | book on t;
 assert TransactionsDontGetStuck = always forall t: Transaction | (t is initialized => eventually t is finalized);

diff --git a/examples/paper/example/transaction.alle b/examples/paper/example/transaction.alle
diff --git a/examples/paper/performance/rebel/RiverCrossing.rebel b/examples/paper/performance/rebel/RiverCrossing.rebel
@@ -3,24 +3,25 @@ module paper::performance::rebel::RiverCrossing
 spec Cargo
   eats: ?Cargo;
 
-  internal event cross()
+  internal event crossToFar()
+  internal event crossToNear()
 
-  assume DontBeAloneWithFood = always forall c1:Cargo, c2: Cargo, f:Farmer | (c1 != c2 && c2 = c1.eats =>  
+  assume DontBeAloneWithFood = always forall c1:Cargo, c2: Cargo, f:Farmer | (c2 = c1.eats =>  
     if (c1 is near &&  c2 is near) then f is near 
     else if (c1 is far && c2 is far) then f is far);
 
   states:
-    near -> far: cross;
-    far -> near: cross;
+    near -> far: crossToFar;
+    far -> near: crossToNear;
 
 spec Farmer
   event crossAlone()
 
   event crossToFar(cargo: Cargo)
-    pre: cargo is near, cargo.cross();
+    pre: cargo.crossToFar();
 
   event crossToNear(cargo: Cargo)
-      pre: cargo is far, cargo.cross();
+      pre: cargo.crossToNear();
 
   states:
     near -> far: crossAlone, crossToFar;

diff --git a/examples/paper/performance/rebel/RopeBridge.rebel b/examples/paper/performance/rebel/RopeBridge.rebel
@@ -35,7 +35,6 @@ assert EverybodyCrossedInTheLeastTime
 assert CantGoquicker
   = eventually ((forall a: Adventurer | a is far) && (exists t: Torch | t.totalTimeSpend < 17));
 
-
 config EverybodyNear
   = a1,a2,a3,a4: Adventurer is near, 
     t: Torch is near with totalTimeSpend = 0,

diff --git a/examples/paper/sepact/messages/checks/CTChecks.rebel b/examples/paper/sepact/messages/checks/CTChecks.rebel
@@ -22,7 +22,7 @@ config SingleCT = p1,p2:Party,
 
 spec MockIBAN
 
-config SimpleCT = ib1,ib2:MockIBAN abstracts IBAN, 
+config SimpleCT = ib1,ib2:MockIBAN mocks IBAN, 
                   m: Money,
                   d: Date,  
                   ct: CustomerCreditTransferRequest forget originator, remittanceInfo,