From 92d3f379889fda5536faa57dc23bd8649c57d702 Mon Sep 17 00:00:00 2001 From: Jouke Stoel Date: Tue, 27 Oct 2020 09:58:40 +0100 Subject: [PATCH] Some cleanup --- examples/paper/example/Person.rebel | 21 ---- examples/paper/example/Transaction.rebel | 6 +- examples/paper/example/transaction.alle | 100 ------------------ .../performance/rebel/RiverCrossing.rebel | 13 +-- .../paper/performance/rebel/RopeBridge.rebel | 1 - .../sepact/messages/checks/CTChecks.rebel | 2 +- 6 files changed, 11 insertions(+), 132 deletions(-) delete mode 100644 examples/paper/example/Person.rebel delete mode 100644 examples/paper/example/transaction.alle diff --git a/examples/paper/example/Person.rebel b/examples/paper/example/Person.rebel deleted file mode 100644 index 95f168d..0000000 --- a/examples/paper/example/Person.rebel +++ /dev/null @@ -1,21 +0,0 @@ -module paper::example::Person - -spec Person - age: Integer, - spouse: ?Person; - - event marry(other: Person) - pre: this.spouse = none, other != this, other.age >= 18; - post: this.spouse' = other; - - states: - single -> married: marry; - -assert CanMarry = eventually exists p: Person | p is married; -assert CanNotBeMarriedToSelf = always forall p:Person | (p is married => p.spouse != p); - -config TwoPersons = p1,p2: Person is single; - -run CanMarry from TwoPersons in max 1 steps; - -check CanNotBeMarriedToSelf from TwoPersons in max 5 steps; diff --git a/examples/paper/example/Transaction.rebel b/examples/paper/example/Transaction.rebel index f3ae865..6a7f61c 100644 --- 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 deleted file mode 100644 index 8cf280b..0000000 --- a/examples/paper/example/transaction.alle +++ /dev/null @@ -1,100 +0,0 @@ -Config (c:id) = {,} -trans (frm:id,to:id) = {} -first (c:id) = {} - -Transaction (inst:id) = {} // immutable -frm (c:id,inst:id,f:id) <= {,,,} // var -to (c:id,inst:id,f:id) <= {,,,} // var -amt (c:id,inst:id,f:id) <= {,,,} // var -tstate (c:id,inst:id,f:id) <= {,,,,,,,}//var -amt_val (f:id,val:int) <= {,} // immutable -TState (state:id) = {,,,} // immutable - -Account (inst:id) = {,} // immutable -astate (c:id,inst:id,f:id) <= {..} // var -bal (c:id,inst:id,f:id) <= {..} //var -bal_val (f:id, val:int) <= {..} // var -AState (state:id) = {} // immutable - -Initialized (state:id) = {,,} // immutable -State_Created (state:id) = {} // immutable -State_Opened (state:id) = {} // immutable - -Events (event:id) = {,,,,} // immutable -Event_Create (event:id) = {} // immutable -Event_Book (event:id) = {} // immutable -Event_Withdraw (event:id) = {} // immutable -Event_Deposit (event:id) = {} // immutable - -Raised (c:id,inst:id,event:id) <= {,,,,,} //var -ChangeSet (c:id,inst:id) <= {..,..,..} - -// Transaction Domain and Multiplicity constraints -frm ⊆ Config ⨯ Transaction ⨯ Account[inst as f] -∀ c ∈ Config | ∀ t ∈ Transaction | (((t ⨯ c) ⨝ tstate)[f->state] ⊆ Initialized ⇔ one (t ⨯ c) ⨝ frm) - -to ⊆ Config ⨯ Transaction ⨯ Account[inst as f] -∀ c ∈ Config | ∀ t ∈ Transaction | (((t ⨯ c) ⨝ tstate)[f->state] ⊆ Initialized ⇔ one (t ⨯ c) ⨝ to) - -amt ⊆ Config ⨯ Transaction ⨯ amt_val[f] -∀ c ∈ Config | ∀ t ∈ Transaction | (((t ⨯ c) ⨝ tstate)[f->state] ⊆ Initialized ⇔ one (t ⨯ c) ⨝ amt ⨝ amt_val) - -// Account Domain and Multiplicity constraints -bal ⊆ Config ⨯ Account ⨯ bal_val[f] -∀ c ∈ Config | ∀ ac ∈ Account | (((ac ⨯ c) ⨝ astate)[f->state] ⊆ Initialized ⇔ one (ac ⨯ c) ⨝ bal ⨝ bal_val) - -// Every transition has one raised event -no Raised ⨝ first -∀ c ∈ Config ∖ first | one Raised ⨝ c - -∀ cur ∈ Config | let prev = (cur[c as to] ⨝ trans)[frm->c] | - // Booked Event - ∀ t ∈ Transaction | (((cur ⨝ Raised)[inst] = t ∧ (cur ⨝ Raised)[event] = Event_Book) ⇒ ( - - // Synchronize with frm.withdraw - ((((prev ⨯ t) ⨝ frm)[f->inst] ⨯ prev) ⨝ astate)[inst] = ((((cur ⨯ t) ⨝ frm)[f->inst] ⨯ cur) ⨝ astate)[inst] ∧ - some (((((prev ⨯ t) ⨝ frm)[f->inst] ⨯ prev) ⨝ bal ⨝ bal_val)[val->prev_val] ⨯ ((((cur ⨯ t) ⨝ frm)[f->inst] ⨯ cur) ⨝ bal ⨝ bal_val)[val->cur_val]) where (cur_val = prev_val - 10) ∧ - - // Synchronize with to.deposit - ((((prev ⨯ t) ⨝ to)[f->inst] ⨯ prev) ⨝ astate)[inst] = ((((cur ⨯ t) ⨝ to)[f->inst] ⨯ cur) ⨝ astate)[inst] ∧ - some (((((prev ⨯ t) ⨝ to)[f->inst] ⨯ prev) ⨝ bal ⨝ bal_val)[val->prev_val] ⨯ ((((cur ⨯ t) ⨝ to)[f->inst] ⨯ cur) ⨝ bal ⨝ bal_val)[val->cur_val]) where (cur_val = prev_val + 10) ∧ - - // Post condition - (prev ⨝ tstate ⨝ t)[f] = (cur ⨝ tstate ⨝ t)[f] ∧ - (prev ⨝ amt ⨝ t)[f] = (cur ⨝ amt ⨝ t)[f] ∧ - (prev ⨝ frm ⨝ t)[f] = (cur ⨝ frm ⨝ t)[f] ∧ - (prev ⨝ to ⨝ t)[f] = (cur ⨝ to ⨝ t)[f]) - ) - -// Synchronization ChangeSet constraint -∀ c ∈ Config | let prev = (c[c as to] ⨝ trans)[frm->c] | - // Booked Event - ∀ t ∈ Transaction | ( - // Book Event - (((c ⨝ Raised)[inst] = t ∧ (c ⨝ Raised)[event] = Event_Book) ⇒ ( - (ChangeSet ⨝ c)[inst] = t ∪ (t ⨝ frm ⨝ prev)[f->inst] ∪ (t ⨝ to ⨝ prev)[f->inst] - )) ∧ - // Create Event - (((c ⨝ Raised)[inst] = t ∧ (c ⨝ Raised)[event] = Event_Create) ⇒ ( - (ChangeSet ⨝ c)[inst] = t - )) - ) - -// Frame values -∀ c ∈ Config | let prev = (c[c as to] ⨝ trans)[frm->c] | - ∀ t ∈ Transaction | (no t ∩ (ChangeSet ⨝ c)[inst] ⇒ ( - (prev ⨝ tstate ⨝ t)[f] = (c ⨝ tstate ⨝ t)[f] ∧ - (prev ⨝ amt ⨝ t)[f] = (c ⨝ amt ⨝ t)[f] ∧ - (prev ⨝ frm ⨝ t)[f] = (c ⨝ frm ⨝ t)[f] ∧ - (prev ⨝ to ⨝ t)[f] = (c ⨝ to ⨝ t)[f]) - ) ∧ - ∀ ac ∈ Account | (no ac ∩ (ChangeSet ⨝ c)[inst] ⇒ ( - (prev ⨝ astate ⨝ ac)[f] = (c ⨝ astate ⨝ ac)[f] ∧ - (prev ⨝ bal ⨝ ac)[f] = (c ⨝ bal ⨝ ac)[f]) - ) - -// Assert: CanBookATransaction -∃ c ∈ Config, t ∈ Transaction | (Raised ⨝ c ⨝ t)[event] = Event_Book - -(first ⨝ tstate)[f->state] = State_Created - \ No newline at end of file diff --git a/examples/paper/performance/rebel/RiverCrossing.rebel b/examples/paper/performance/rebel/RiverCrossing.rebel index 9fc3af3..e8b9aab 100644 --- 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 index 4de38d7..04c41b3 100644 --- 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 index 2b84bb8..b4550f3 100644 --- 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,