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

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

On Wed, Jun 19, 2024 at 10:55 AM Lee <fowler.lee8@xxxxxxxxx> wrote:

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

--
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/4a42707b-1bcf-4b53-99c3-3c5eede1da4cn%40googlegroups.com.