let four_phase_handshake_nets = [ ("Strobe", Output, Concrete_enum ["true"; "false"]); ("Ack", Input, Concrete_enum ["true"; "false"]); ("DL", Output, Symbolic_bitvec (8) ) ] let four_phase_handshake_idle = [ ("dead", "DL"); ("false", "Strobe"); ("false", "Ack") ] ; let four_phase_handshake_protocol = Seq[ Set("live", "DL"); Set("true", "Strobe"); Set("true", "Ack"); Set("dead", "DL"); Set("false", "Strobe"); Set("false", "Ack") ] ; (* Overall composition of the protocol in a direction-agnostic form *) let fourphase = ("4P", four_phase_handshake_nets, four_phase_handshake_idle, four_phase_handshake_protocol)