(**
  Spanning Tree Algorithm: the sync breadth-first search

  (local variables)
  int visited, depth <- 0
  int parent <- _|_
  set of int Neighbors <- set of neighbors

  (message types)
  QUERY

  1) if i = root then
  2)   visited <- 1;
  3)   depth <- 0;
  4)   send QUERY to Neighbors;
  5) for round = 1 to diameter do
  6)   if visited = 0 then
  7)     if any QUERY messages arrive then
  8)       parent <- randomly select a node from which
                     QUERY was received;
  9)       visited <- 1;
  10)      depth <- round;
  11)      send QUERY to Neighbors \ {senders of QUERYs received
                                      in this round};
  12)  delete any QUERY messages that arrive in this round;
**)

(** Data Structure **)
{  { 1 <- value, {}      <- parents  , {2,3}   <- childrens }
 , { 2 <- value, {1}     <- parents  , {4,3}   <- childrens }
 , { 3 <- value, {4, 2}  <- parents  , {5,6}   <- childrens }
 , { 4 <- value, {1,2,3} <- parents  , {5}     <- childrens }
 , { 5 <- value, {4,3}   <- parents  , {6}     <- childrens }
 , { 6 <- value ,{3,5}   <- parents  , {}      <- childrens } }

VARIABLES nodes
CONSTANT Val

(** Data Structure Input **)
(** { value, parents, children } **)
Val <-
{   { 1 , {}      , {2,3} }
  , { 2 , {1}     , {4,3} }
  , { 3 , {4, 2}  , {5,6} }
  , { 4 , {1,2,3} , {5}   }
  , { 5 , {4,3}   , {6}   }
  , { 6 , {3,5}   , {}    } }

TypeInvariant == /\
     \A node \in nodes
           : node \in [  value     \in Nat
                       , parents   \in Nat
                       , childrens \in Nat
                       , visited   :  {0,1}
                       , depth     :  {0,1} ]

Init == /\ nodes = {}

Insert(v) ==
	/\ \A node \in nodes : node.value = v[0] == {}
        /\ nodes' = nodes \union
			{  value     : v[0]
                         , parents   : v[1]
                         , childrens : v[2]
                         , visited   : 0
                         , depth     : 0 }

Next ==
	/\ \E node \in Val : Insert(v)

Spec == Init \/ [][Next]_<<nodes>> \/ TRUE