Question: how to describe the network message from ewd687a/EWD687aPlusCal.tla in Rust?

[Lee]

Hello All,

The following is a question about how to implement a certain piece of TLA+ in Rust, Python, Java Or Go (any language will do, I just need to get my head around it):

I am implementing the algorithm ewd687a/EWD687aPlusCal.tla from the Specifications listed on GitHub for the TLAExamples repo. I am having difficulty describing the TLA+ statement for the network in Rust (see below):

This is the statement in the spec and the part I find tricky is: msg->[snd \in Node |-> 0]: 

(* For every node we keep the following counters:

- number of base messages received, per sending node

- number of ack messages received *)

network = [n \in Node |-> [msg |-> [snd \in Node |-> 0], ack |-> 0]]

My hope is to get some guidance on how one might describe the network as a struct in the form:

struct Message {

from: Node,

ack: u16,

}

#[derive(Debug, Clone)]

pub struct Node {

pub name: String,

active: bool,

node: Option<Rc<RefCell<Node>>>,

message: u32,

ack: u32,

}

struct Network {

network: VecDeque<Node>,

status: Vec<Message>,

termination_detection: bool,

}

________________________________________

I probably have it quite wrong so thank you for any tips you can provide.

King Greetings

Lee F

[Markus Kuppe]

Hi Lee,

I don't have time for a longer response, but you might find some inspiration from my Java implementation [1] of EWD998 (also distributed termination detection).

Markus

[1] https://github.com/tlaplus/Examples/blob/master/specifications/ewd998/impl/src/EWD998.java

> --
> You received this message because you are subscribed to the Google Groups "tlaplus" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/4a42707b-1bcf-4b53-99c3-3c5eede1da4cn%40googlegroups.com.

[Lee]

Thank you for your response Markus, this will surely help. 

\Lee

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/A4C3654D-FD8B-46EF-B3F2-A08036907F2D%40lemmster.de.

[Finn Hackett]

I notice your example has various additional parts that indicate what you probably think is useful in an implementation (and you are probably right). If I was stuck at this point, perhaps shrinking it all down to the simplest possible interpretation (then building back up) would get me un-stuck.

Here's a minimal Scala implementation that reflects just the TLA+ and nothing more. Keep in mind I coded this in my e-mail client.

type NodeId = Int // to mark where I'm translating x \in Node

// [msg |-> [snd \in Node |-> 0], ack |-> 0

case class NodeState(

  msg: Map[NodeId, Int], // [snd \in Node |-> 0]

  ack: Int) // ack |-> 0

// [n \in Node |-> ...]

type Network = Map[NodeId, NodeState]

... of course, the glaring problem is that this has nothing to do with an actual network, but starting from something super simplified like this and adding / replacing (a lot of) details might get you there.

-Finn

--

[Lee]

Thanks for the tip Finn, i now better understand the approach. Cheers!

/Lee

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAJs285%3DoX0-LrG2XhD9raUvCTtfH7tKrO7h%3DApKESUYVhxdojw%40mail.gmail.com.