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 |-> 0case 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 GreetingsLee 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.
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/CAJs285%3DoX0-LrG2XhD9raUvCTtfH7tKrO7h%3DApKESUYVhxdojw%40mail.gmail.com.