Skip to content

Commit

Permalink
Merge branch 'main' into gabriela/type-aliases
Browse files Browse the repository at this point in the history
  • Loading branch information
@bugarela
bugarela authored Dec 5, 2022
2 parents c8b7e73 + a0ac348 commit f687fd6
Show file tree
Hide file tree
Showing 22 changed files with 600 additions and 301 deletions.
92 changes: 47 additions & 45 deletions examples/LamportMutex/LamportMutex.tnt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -44,11 +44,11 @@ module LamportMutex {
val Message = Set(AckMessage, RelMessage).union(Clock.map(c => ReqMessage(c)))

action Init = all {
clock <- Proc.mapBy(p => 0),
req <- Proc.mapBy(p => Proc.mapBy(q => 0)),
ack <- Proc.mapBy(p => Set()),
network <- Proc.mapBy(p => Proc.mapBy(q => List())),
crit <- Set(),
clock' = Proc.mapBy(p => 0),
req' = Proc.mapBy(p => Proc.mapBy(q => 0)),
ack' = Proc.mapBy(p => Set()),
network' = Proc.mapBy(p => Proc.mapBy(q => List())),
crit' = Set(),
}

/* beats(p,q) is true if process p believes that its request has higher
Expand All @@ -73,11 +73,11 @@ module LamportMutex {
// Process p requests access to critical section.
action Request(p) = all {
req.get(p).get(p) == 0,
req <- req.setBy(p, r => r.setBy(p, c => clock.get(p))),
network <- network.setBy(p, n => Broadcast(p, ReqMessage(clock.get(p)))),
ack <- ack.set(p,Set(p)),
clock <- clock,
crit <- crit,
req' = req.setBy(p, r => r.setBy(p, c => clock.get(p))),
network' = network.setBy(p, n => Broadcast(p, ReqMessage(clock.get(p)))),
ack' = ack.set(p,Set(p)),
clock' = clock,
crit' = crit,
}

// Process p receives a request from q and acknowledges it.
Expand All @@ -87,79 +87,81 @@ module LamportMutex {
val c = m.clock
all {
m.mtype == "req",
req <- req.setBy(p, a => a.setBy(q, b => c)),
clock <- clock.setBy(p, a => if (c > a) c + 1 else a + 1),
network <- network.setBy(q, a => a.setBy(p, b => b.tail()))
req' = req.setBy(p, a => a.setBy(q, b => c)),
clock' = clock.setBy(p, a => if (c > a) c + 1 else a + 1),
network' = network.setBy(q, a => a.setBy(p, b => b.tail()))
.setBy(p, a => a.setBy(q, b => b.append(AckMessage))),
},
ack <- ack,
crit <- crit,
ack' = ack,
crit' = crit,
}

// Process p receives an acknowledgement from q.
action ReceiveAck(p, q) = all {
network.get(p).get(q) != List(),
val m = network.get(p).get(q).head() all {
m.mtype == "ack",
network <- network.setBy(p, a => a.setBy(q, b => b.tail())),
ack <- ack.setBy(p, a => a.union(Set(q))),
network' = network.setBy(p, a => a.setBy(q, b => b.tail())),
ack' = ack.setBy(p, a => a.union(Set(q))),
},
clock <- clock,
req <- req,
crit <- crit,
clock' = clock,
req' = req,
crit' = crit,
}

// Process p enters the critical section.
action Enter(p) = all {
ack.get(p) == Proc,
Proc.forall(q => beats(p, q)),
crit <- crit.union(Set(p)),
clock <- clock,
req <- req,
ack <- ack,
network <- network,
crit' = crit.union(Set(p)),
clock' = clock,
req' = req,
ack' = ack,
network' = network,
}

// Process p exits the critical section and notifies other processes.
action Exit(p) = all {
p.in(crit),
crit <- crit.exclude(Set(p)),
network <- network.set(p, Broadcast(p, RelMessage)),
req <- req.setBy(p, r => r.set(p, 0)),
ack <- ack.set(p, Set()),
clock <- clock,
crit' = crit.exclude(Set(p)),
network' = network.set(p, Broadcast(p, RelMessage)),
req' = req.setBy(p, r => r.set(p, 0)),
ack' = ack.set(p, Set()),
clock' = clock,
}

// Process p receives a release notification from q.
action ReceiveRelease(p,q) = all {
network.get(p).get(q) != List(),
val m = network.get(p).get(q).head() all {
m.mtype == "rel",
req <- req.setBy(p, r => r.set(q, 0)),
network <- network.setBy(p, a => a.setBy(q, b => b.tail())),
req' = req.setBy(p, r => r.set(q, 0)),
network' = network.setBy(p, a => a.setBy(q, b => b.tail())),
},
clock <- clock,
ack <- ack,
crit <- crit,
clock' = clock,
ack' = ack,
crit' = crit,
}

// Next-state relation.
action Next = any {
Proc.guess(p => any {
action Next = {
nondet p = oneOf(Proc)
any {
Request(p),
Enter(p),
Exit(p),
}),
Proc.guess(p => Proc.guess(q => any {
ReceiveRequest(p,q),
ReceiveAck(p,q),
ReceiveRelease(p,q),
})),
}
nondet q = oneOf(Proc)
any {
ReceiveRequest(p,q),
ReceiveAck(p,q),
ReceiveRelease(p,q),
}
}
}

/* A state constraint that is useful for validating the specification
using finite-state model checking. */
val ClockConstraint = Proc.forall(p => clock.get(p) <= maxClock)
val ClockConstraint = Proc.forall(p => (clock.get(p) <= maxClock))

/* No channel ever contains more than three messages. In fact, no channel
ever contains more than one message of the same type, as proved below.*/
Expand Down
78 changes: 41 additions & 37 deletions examples/Paxos/Paxos.tnt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -101,18 +101,18 @@ val TypeOK = and {
}

action Init = all {
maxBal <- Acceptor.mapBy(_ => -1),
maxVBal <- Acceptor.mapBy(_ => -1),
maxVal <- Acceptor.mapBy(_ => None),
msgs <- Set(),
maxBal' = Acceptor.mapBy(_ => -1),
maxVBal' = Acceptor.mapBy(_ => -1),
maxVal' = Acceptor.mapBy(_ => None),
msgs' = Set(),
}

/***************************************************************************)
(* The actions. We begin with the subaction (an action that will be used *)
(* to define the actions that make up the next-state action. *)
(***************************************************************************/
action Send(m) = {
msgs <- msgs.union(Set(m))
msgs' = msgs.union(Set(m))
}

/***************************************************************************)
Expand All @@ -123,8 +123,8 @@ action Send(m) = {
(***************************************************************************/
action Phase1a(b) = all {
Send({ tag: "1a", bal: b }),
maxVBal <- maxVBal,
maxVal <- maxVal,
maxVBal' = maxVBal,
maxVal' = maxVal,
}

/***************************************************************************)
Expand All @@ -134,15 +134,15 @@ action Phase1a(b) = all {
(* maxVBal[a] and maxVal[a]. *)
(***************************************************************************/
action Phase1b(a) = {
msgs.filter(m => m.tag == "1a")
.guess(m => all {
m.bal > maxBal.get(a),
maxBal <- maxBal.set(a, m.bal),
Send({ tag: "1b", acc: a, bal: m.bal,
mbal: maxVBal.get(a), mval: maxVal.get(a) }),
maxVBal <- maxVBal,
maxVal <- maxVal,
})
nondet m = msgs.filter(m2 => m2.tag == "1a").oneOf()
all {
m.bal > maxBal.get(a),
Send({ tag: "1b", acc: a, bal: m.bal,
mbal: maxVBal.get(a), mval: maxVal.get(a) }),
maxBal' = maxBal.set(a, m.bal),
maxVBal' = maxVBal,
maxVal' = maxVal,
}
}

/***************************************************************************)
Expand Down Expand Up @@ -184,8 +184,8 @@ action Phase2a(b, v) = all {
}
),
Send({ tag: "2a", bal: b, value: v }),
maxVBal <- maxVBal,
maxVal <- maxVal,
maxVBal' = maxVBal,
maxVal' = maxVal,
}

/***************************************************************************)
Expand All @@ -197,15 +197,16 @@ action Phase2a(b, v) = all {
(* phase 2b message announcing its vote. It also sets maxBal[a] to the *)
(* message's. ballot number *)
(***************************************************************************/
action Phase2b(a) = msgs.filter(m => m.tag == "2a")
.guess(m => all {
m.bal >= maxBal.get(a),
maxBal <- maxBal.set(a, m.bal),
maxVBal <- maxVBal.set(a, m.bal),
maxVal <- maxVal.set(a, m.value),
Send({ tag: "2b", acc: a,
bal: m.bal, value: m.value }),
})
action Phase2b(a) = {
nondet m = msgs.filter(m2 => m2.tag == "2a").oneOf()
all {
m.bal >= maxBal.get(a),
Send({ tag: "2b", acc: a, bal: m.bal, value: m.value }),
maxBal' = maxBal.set(a, m.bal),
maxVBal' = maxVBal.set(a, m.bal),
maxVal' = maxVal.set(a, m.value),
}
}

/***************************************************************************)
(* In an implementation, there will be learner processes that learn from *)
Expand All @@ -217,17 +218,20 @@ action Phase2b(a) = msgs.filter(m => m.tag == "2a")
(* Below are defined the next-state action and the complete spec. *)
(***************************************************************************/
action Next = any {
all {
Ballot.guess(b => any {
Phase1a(b),
Value.guess(v => Phase2a(b, v)),
}),
maxBal <- maxBal,
all {
nondet b = oneOf(Ballot)
any {
Phase1a(b),
nondet v = oneOf(Value)
Phase2a(b, v)
},
Acceptor.guess(a => any {
Phase1b(a),
Phase2b(a),
}),
maxBal' = maxBal,
},
nondet a = oneOf(Acceptor)
any {
Phase1b(a),
Phase2b(a),
}
}

temporal Spec = Init and always(stutter(Next, vars))
Expand Down
27 changes: 15 additions & 12 deletions examples/Paxos/Voting.tnt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -164,8 +164,8 @@ THEOREM ShowsSafety ==
(* straightforward. *)
(***************************************************************************/
action Init = all {
votes <- Acceptor.mapBy(_ => Set()),
maxBal <- Acceptor.mapBy(_ => -1),
votes' = Acceptor.mapBy(_ => Set()),
maxBal' = Acceptor.mapBy(_ => -1),
}


Expand All @@ -177,8 +177,8 @@ action Init = all {
(***************************************************************************/
action IncreaseMaxBal(a, b) = all {
b > maxBal.get(a),
maxBal <- maxBal.set(a, b),
votes <- votes,
maxBal' = maxBal.set(a, b),
votes' = votes,
}

/***************************************************************************)
Expand All @@ -196,20 +196,23 @@ action VoteFor(a, b, v) = all {
votes.get(c).forall( vt => (vt._1 == b) implies (vt._2 == v) )
),
Quorum.exists( Q => ShowsSafeAt(Q, b, v) ),
votes <- votes.setBy(a, old => old.union(Set((b, v))) ),
maxBal <- maxBal.set(a, b),
votes' = votes.setBy(a, old => old.union(Set((b, v))) ),
maxBal' = maxBal.set(a, b),
}


/***************************************************************************)
(* The next-state action and the invariant. *)
(***************************************************************************/
action Next =
tuples(Acceptor, Ballot).guess((a, b) => any {
IncreaseMaxBal(a, b),
Value.guess(v => VoteFor(a, b, v)),
}
)
action Next = {
nondet a = oneOf(Acceptor)
nondet b = oneOf(Ballot)
any {
IncreaseMaxBal(a, b),
nondet v = oneOf(Value)
VoteFor(a, b, v),
}
}

temporal Spec = Init and always(stutter(Next, (votes, maxBal)))

Expand Down
Loading

0 comments on commit f687fd6

Please sign in to comment.