--
-- $Id: nodes_bmc.smv.in,v 1.1 2006/05/24 00:12:59 schuppan Exp $
--

--------------------------------------------------------------------------
-- start configurable parameters                                        --
--------------------------------------------------------------------------

-- define enables/undef disables symmetry reduction
@symmetry@ USE_SYMMETRY

-- define enables/undef disables bounded model checking
@bmc@ USE_BMC

-- the number of nodes of the model
#define NUMNODES @numnodes@

-- the number of ports per node of the model
#define NUMPORTS @numports@

-- number of unsuccessful iterations through the root contention protocol
-- only for bounded model checking
#define ROOTCONT_ITS @rootcontits@



-- define enables/undef disables force-root determinism
@forcerootdet@ FORCE_ROOT_DET

-- define enables/undef disables configuration determinism
@configurationdet@ CONFIGURATION_DET

-- define enables/undef disables cycle in configuration with 6 nodes and
-- 4 ports
@sixnocycle@ SIX_NO_CYCLE

-- define enables/undef disables additional assertions
#undef VERIFY_NOROOTCHANGE
#undef VERIFY_FORCEROOTEFFECT
#undef VERIFY_DETECTCYCLES

--------------------------------------------------------------------------
-- end configurable parameters                                          --
--------------------------------------------------------------------------

#define MAXNODE (NUMNODES - 1)
#define MAXPORT (NUMPORTS - 1)

#define FORCEROOT_CYCLES (3 * (NUMNODES - 2) + 1)
#define TIMEOUT_CYCLES (FORCEROOT_CYCLES + 3 * ((NUMNODES - 1) / 2) + 1)
#define DIFFERENT_CYCLES (TIMEOUT_CYCLES + 5 + ROOTCONT_ITS * 4 - 1)
#ifndef USE_BMC
#define RANGE_CYCLES (TIMEOUT_CYCLES + 1)
#else
#define RANGE_CYCLES (DIFFERENT_CYCLES + 1)
#endif

#ifdef USE_SYMMETRY
  scalarset PORT 0..MAXPORT;
  scalarset NODE 0..MAXNODE;
#else
  typedef PORT 0..MAXPORT;
  typedef NODE 0..MAXNODE;
#endif


--
-- node.smv
--


--
-- port.smv
--

module port()
  
{
  cin:  {idle, parent_notify, child_notify};
  cout: {idle, parent_notify, child_notify};
  role: {off, unknown, child, parent};
  pnode: NODE;
  pport: PORT;

  init(cout) := idle;
#ifndef CONFIGURATION_DET
  init(role) := { off, unknown };
  next(pnode) := pnode;
  next(pport) := pport;
#endif
}


module node()

{
  port: array PORT of port;
  state: {T0_start, T1_child, T2_parent, T3_root_1, T3_root_2, T3_root_3, S0_start};
  is_root: boolean;
  force_root: boolean;
  rnd: boolean;
  timeout: boolean;
  cycles: 0..RANGE_CYCLES;
  tmp, tmp2, tmp3: array PORT of boolean;
  tmp4: array PORT of array PORT of boolean;

  init(state) := T0_start;
  init(is_root) := 0;
  init(timeout) := 0;
  init(cycles) := 0;

  ------------------------------------------------------------------------
  ------------------------------------------------------------------------
  -- state
  ------------------------------------------------------------------------
  ------------------------------------------------------------------------

  default {
    next(state) := state;
  }
  in switch(state) {

    ----------------------------------------------------------------------
    -- T0_start
    ----------------------------------------------------------------------
    T0_start: {
      forall(i in PORT) {
        forall(j in PORT) {
	  tmp4[i][j] := (i ~= j) -> ~((port[i].role = unknown) & (port[j].role = unknown));
	}
	tmp[i] := &tmp4[i];
      }
      if ((&tmp) & (force_root -> cycles > FORCEROOT_CYCLES))
	next(state) := T1_child;   
    }

    ----------------------------------------------------------------------
    -- T1_child
    ----------------------------------------------------------------------
    T1_child: {
      forall(i in PORT) {
	tmp[i] := port[i].role = child -> port[i].cin = idle;
      }
      if (&tmp)
	next(state) := T2_parent;
    }

    ----------------------------------------------------------------------
    -- T2_parent
    ----------------------------------------------------------------------
    T2_parent: {
      forall(i in PORT) {
	tmp[i] := port[i].role = unknown -> port[i].cin = child_notify;
      }
      forall(i in PORT) {
	tmp2[i] := port[i].role = unknown -> port[i].cin = parent_notify;
      }
      if (&tmp)
	next(state) := S0_start;
      else if (&tmp2)
	next(state) := T3_root_1;
    }

    ----------------------------------------------------------------------
    -- T3_root_1
    ----------------------------------------------------------------------
    T3_root_1: {
      if (~rnd)
	next(state) := T3_root_3;
      else if (rnd)
	next(state) := T3_root_2;
    }

    ----------------------------------------------------------------------
    -- T3_root_2
    ----------------------------------------------------------------------
    T3_root_2: {
      next(state) := T3_root_3;
    }

    ----------------------------------------------------------------------
    -- T3_root_3
    ----------------------------------------------------------------------
    T3_root_3: {
      forall(i in PORT) {
	tmp[i] := port[i].role = unknown -> port[i].cin = idle;
      }
      forall(i in PORT) {
	tmp2[i] := port[i].role = unknown -> port[i].cin = parent_notify;
      }
      if (&tmp)
	next(state) := T2_parent;
      else if (&tmp2)
	next(state) := T1_child;
    }

  }

  ------------------------------------------------------------------------
  ------------------------------------------------------------------------
  -- is_root
  ------------------------------------------------------------------------
  ------------------------------------------------------------------------

  default {
    next(is_root) := is_root;
  }
  in switch(state) {

    T1_child: {
      forall(i in PORT) {
	tmp3[i] := port[i].role = unknown;
      }
      if (|tmp3)
	next(is_root) := 0;
      else
	next(is_root) := 1;
    }

  }

  ------------------------------------------------------------------------
  ------------------------------------------------------------------------
  -- port[].cout
  ------------------------------------------------------------------------
  ------------------------------------------------------------------------

  forall(i in PORT) {

    default {
      next(port[i].cout) := port[i].cout;
    } in switch (state) {

      -- T1_child
	T1_child: {
	if (port[i].role = child)
	  next(port[i].cout) := child_notify;
	else if (port[i].role = unknown)
	  next(port[i].cout) := parent_notify;
      }
      
      -- T3_root_1
	T3_root_1: {
	if (port[i].role = unknown)
	  next(port[i].cout) := idle;
      }
      
      -- T3_root_3
	T3_root_3: {
	if (port[i].role = unknown & port[i].cin = idle)
	  next(port[i].cout) := parent_notify;
      }
      
      -- S0_start
	S0_start: {
	if ((port[i].role = parent & port[i].cin = child_notify) |
	    (port[i].role = child & port[i].cin = idle) |
	    (is_root))
	  next(port[i].cout) := idle;
      }
      
    }

  }

  ------------------------------------------------------------------------
  ------------------------------------------------------------------------
  -- port[].role
  ------------------------------------------------------------------------
  ------------------------------------------------------------------------

  forall(i in PORT) {

    default {
      next(port[i].role) := port[i].role;
    } in switch (state) {
      
    T0_start: {
      if (port[i].role = unknown & port[i].cin = parent_notify)
	next(port[i].role) := child;
    }
    
    T2_parent: {
      if (port[i].role = unknown & port[i].cin = child_notify)
	next(port[i].role) := parent;
    }
    
    T3_root_3: {
      if (port[i].role = unknown & port[i].cin = parent_notify)
	next(port[i].role) := child;
    }
    
    }

  }

  ------------------------------------------------------------------------
  ------------------------------------------------------------------------
  -- force_root
  ------------------------------------------------------------------------
  ------------------------------------------------------------------------

#ifndef FORCE_ROOT_DET
  next(force_root) := force_root;
#endif

  ------------------------------------------------------------------------
  ------------------------------------------------------------------------
  -- rnd
  ------------------------------------------------------------------------
  ------------------------------------------------------------------------

  if (state = T2_parent) {
    next(rnd) := {0, 1};
  }
  else {
    next(rnd) := rnd;
  }

  ------------------------------------------------------------------------
  ------------------------------------------------------------------------
  -- timeout
  ------------------------------------------------------------------------
  ------------------------------------------------------------------------

  next(timeout) := timeout | state = T0_start & cycles > TIMEOUT_CYCLES;

  ------------------------------------------------------------------------
  ------------------------------------------------------------------------
  -- cycles
  ------------------------------------------------------------------------
  ------------------------------------------------------------------------

  if (state = T0_start) {
    next(cycles) := (cycles + 1) <= RANGE_CYCLES ? cycles + 1 : cycles;
  }
  else {
    next(cycles) := cycles;
  }

}


--
-- nodes.smv
--

module main()

{
  nodes: array NODE of node;
  timeout: array NODE of boolean;
  known_problems: boolean;
  orphan: array NODE of boolean;
  in_state_S0_start: array NODE of boolean;
  at_least_one_root: array NODE of boolean;
  at_most_one_root: boolean;
  roles_determined: boolean;
  links_idle: boolean;
#ifdef VERIFY_FORCEROOTEFFECT
  at_most_one_forceroot: boolean;
#endif
  tmp: array NODE of array PORT of boolean;
  tmp2: array NODE of array NODE of boolean;
  tmp3: array NODE of array NODE of boolean;
  tmp4: array NODE of boolean;
  tmp5: array NODE of array PORT of boolean;
  tmp6: array NODE of boolean;
  tmp7: array NODE of array PORT of boolean;
  tmp8: array NODE of boolean;
#ifdef VERIFY_FORCEROOTEFFECT
  tmp9: array NODE of array NODE of boolean;
  tmp10: array NODE of boolean;
#endif

--
-- model.smv
--

--------------------------------------------------------------------------------
-- different                                                                  --
--------------------------------------------------------------------------------

#ifndef USE_BMC
  different: boolean;

  if (different) next(different) := different;

  different_fairness: assert G F different;
#else
  cycles2: 0..RANGE_CYCLES;
  different: boolean;

  init(cycles2) := 0;
  init(different) := 0;
  next(cycles2) := (cycles2 + 1) <= RANGE_CYCLES ? cycles2 + 1 : cycles2;
  next(different) := cycles2 > DIFFERENT_CYCLES ? 1 : different;
#endif

  different_effect1: array NODE of array NODE of boolean;
  different_effect2: array NODE of boolean;

  forall(m in NODE) {
    forall(n in NODE) {
      different_effect1[m][n] := ((m ~= n) -> ((nodes[m].state = T3_root_1 & nodes[n].state = T3_root_1) -> (different -> (nodes[m].rnd ~= nodes[n].rnd))));
    }
    different_effect2[m] := &different_effect1[m];
  }

  different_effect: assert G &different_effect2;
  
--------------------------------------------------------------------------------
-- map in out                                                                 --
--------------------------------------------------------------------------------

  forall(m in NODE) {
    forall(i in PORT) {
      nodes[m].port[i].cin := nodes[nodes[m].port[i].pnode].port[nodes[m].port[i].pport].cout;
    }
  }

--------------------------------------------------------------------------------
-- sound configuration                                                        --
--------------------------------------------------------------------------------

  sound1: array NODE of array PORT of array NODE of array PORT of boolean;
  sound2: array NODE of array PORT of array NODE of boolean;
  sound3: array NODE of array PORT of boolean;
  sound4: array NODE of boolean;

  forall(m in NODE) {
    forall(i in PORT) {
      forall(n in NODE) {
	forall(j in PORT) {
          sound1[m][i][n][j] := (nodes[m].port[i].role ~= off & nodes[m].port[i].pnode = n & nodes[m].port[i].pport = j) -> (n ~= m & nodes[n].port[j].role ~= off & nodes[n].port[j].pnode = m & nodes[n].port[j].pport = i);
	}
        sound2[m][i][n] := &sound1[m][i][n];
      }
      sound3[m][i] := &sound2[m][i];
    }
    sound4[m] := &sound3[m];
  }

  sound: assert G &sound4;

--------------------------------------------------------------------------------
-- is connected                                                               --
--------------------------------------------------------------------------------

  is_connected1: array NODE of array NODE of array PORT of boolean;
  is_connected2: array 1..NUMNODES of array NODE of array NODE of boolean;
  is_connected3: array 2..NUMNODES of array NODE of array NODE of array NODE of boolean;
  is_connected4: array NODE of array NODE of boolean;
  is_connected5: array NODE of boolean;

  forall(n in NODE) {
    forall(o in NODE) {
      forall(i in PORT) {
        is_connected1[n][o][i] := nodes[n].port[i].role ~= off & nodes[n].port[i].pnode = o;
      }
      is_connected2[1][n][o] := (|is_connected1[n][o]);
    }
  }
  for(m = 2; m <= NUMNODES; m = m + 1) {
    forall(n in NODE) {
      forall(o in NODE) {
	forall(p in NODE) {
          is_connected3[m][n][o][p] := is_connected2[m-1][n][p] & is_connected2[m-1][p][o];
        }
   	is_connected2[m][n][o] := is_connected2[m-1][n][o] | (|is_connected3[m][n][o]);
      }
    }
  }
  forall(n in NODE) {
    forall(o in NODE) {
      is_connected4[n][o] := n = o | is_connected2[NUMNODES][n][o];
    }
    is_connected5[n] := &is_connected4[n];
  }

  is_connected: assert G &is_connected5;

--------------------------------------------------------------------------------
-- no_cycles                                                                  --
--------------------------------------------------------------------------------

  no_cycles3: array NODE of array PORT of array NODE of array NODE of array PORT of boolean;
  no_cycles4: array NODE of array PORT of array 1..NUMNODES of array NODE of array NODE of boolean;
  no_cycles5: array NODE of array PORT of array 2..NUMNODES of array NODE of array NODE of array NODE of boolean;
  no_cycles6: array NODE of array PORT of boolean;
  no_cycles7: array NODE of boolean;

  forall(m in NODE) {
    forall(i in PORT) {
      forall(n in NODE) {
        forall(o in NODE) {
          forall(j in PORT) {
            no_cycles3[m][i][n][o][j] := ~(nodes[n].port[j].pnode = m & nodes[n].port[j].pport = i | m = n & i ~= j) & (nodes[n].port[j].role ~= off & nodes[n].port[j].pnode = o);
          }
          no_cycles4[m][i][1][n][o] := (|no_cycles3[m][i][n][o]);
        }
      }
      for(l = 2; l <= NUMNODES; l = l + 1) {
        forall(n in NODE) {
          forall(o in NODE) {
	    forall(p in NODE) {
              no_cycles5[m][i][l][n][o][p] := no_cycles4[m][i][l-1][n][p] & no_cycles4[m][i][l-1][p][o];
            }
   	    no_cycles4[m][i][l][n][o] := no_cycles4[m][i][l-1][n][o] | (|no_cycles5[m][i][l][n][o]);
          }
        }
      }
      no_cycles6[m][i] := ~no_cycles4[m][i][NUMNODES][m][m];
    }
    no_cycles7[m] := &no_cycles6[m];
  }

  no_cycles: assert G &no_cycles7;

--
-- spec.smv
--

forall(m in NODE) {
  timeout[m] := nodes[m].timeout;
}

forall(m in NODE) {
  forall(i in PORT) {
    tmp[m][i] := nodes[m].port[i].role = unknown & nodes[m].port[i].cout = parent_notify;
  }
  forall(n in NODE) {
    tmp2[m][n] := m ~= n -> nodes[n].state = S0_start;
  }
  orphan[m] := (|tmp[m]) & (&tmp2[m]) & nodes[m].state = T2_parent;
}
known_problems := |orphan;

forall(m in NODE) {
  in_state_S0_start[m] := nodes[m].state = S0_start;
}

forall(m in NODE) {
  at_least_one_root[m] := nodes[m].is_root;
}

-- FIXME: quadratic complexity
forall(m in NODE) {
  forall(n in NODE) {
   tmp3[m][n] := (m ~= n) -> ~(nodes[m].is_root & nodes[n].is_root);
  }
  tmp4[m] := &tmp3[m];
}
at_most_one_root := &tmp4;

forall(m in NODE) {
  forall(i in PORT) {
    tmp5[m][i] := nodes[m].port[i].role ~= unknown;
  }
  tmp6[m] := &tmp5[m];
}
roles_determined := &tmp6;

forall(m in NODE) {
  forall(i in PORT) {
    tmp7[m][i] := nodes[m].port[i].cout = idle;
  }
  tmp8[m] := & tmp7[m];
}
links_idle := &tmp8;

#ifdef VERIFY_FORCEROOTEFFECT
-- FIXME: quadratic complexity
forall(m in NODE) {
  forall(n in NODE) {
   tmp9[m][n] := (m ~= n) -> ~(nodes[m].force_root & nodes[n].force_root);
  }
  tmp10[m] := &tmp9[m];
}
at_most_one_forceroot := &tmp10;
#endif

--
-- general_spec.smv
--

  -- all nodes are in state S0_start
  ass_in_state_S0_start: assert (F (G (&in_state_S0_start) |
      	(|timeout) |
      	known_problems));

  -- at least one root is elected
  ass_at_least_one_root: assert (F (G (|at_least_one_root) |
      (|timeout) |
      known_problems));

  -- at most one root is elected
  ass_at_most_one_root: assert (F (G (at_most_one_root) |
      (|timeout) |
      known_problems));

  -- all roles are determined
  ass_roles_determined: assert (F (G (roles_determined) |
      (|timeout) |
      known_problems));

  -- all links are idle
  ass_links_idle: assert (F (G (links_idle) |
      (|timeout) |
      known_problems));

#ifdef VERIFY_NOROOTCHANGE
  -- no root change
  forall(m in NODE) { 
    ass_no_root_change[m]: assert (((F nodes[m].is_root) -> (~nodes[m].is_root U nodes[m].is_root)) | 
                                   F ((|timeout) | known_problems));
  }
#endif
#ifdef VERIFY_FORCEROOTEFFECT
  forall(m in NODE) {
    ass_force_root_effect[m]:
      assert at_most_one_forceroot -> (nodes[m].force_root -> F nodes[m].is_root);
  }
#endif
#ifdef VERIFY_DETECTCYCLES
  ass_detect_cycles: assert (!(&no_cycles7)) -> (F (|timeout));
#endif

  -- user spec
  ass_userspec: assert F 1;

  -- no timeout
  ass_no_timeout: assert (G ~(|timeout));

  -- no known problems
  ass_no_known_problems: assert (G ~known_problems);

#ifndef CONFIGURATION_DET
  assume sound;
  assume is_connected;
  assume no_cycles;
#endif
#ifndef USE_BMC
  assume different_fairness;
#endif
  assume different_effect;
  using
    sound,
    is_connected,
    no_cycles,
#ifndef USE_BMC
    different_fairness,
#endif
    different_effect
  prove
    ass_in_state_S0_start,
    ass_at_least_one_root,
    ass_at_most_one_root,
    ass_roles_determined,
    ass_links_idle,
    ass_no_timeout,
    ass_no_known_problems,
    ass_userspec;

#ifdef VERIFY_NOROOTCHANGE
  forall(m in NODE) {
    using
      sound,
      is_connected,
      no_cycles,
#ifndef USE_BMC
      different_fairness,
#endif
      different_effect
    prove
      ass_no_root_change[m];
  }
#endif
#ifdef VERIFY_FORCEROOTEFFECT
  forall(m in NODE) {
    using
      sound,
      is_connected,
      no_cycles,
#ifndef USE_BMC
      different_fairness,
#endif
      different_effect
    prove
      ass_force_root_effect[m];
  }
#endif
#ifdef VERIFY_DETECTCYCLES
  using
    sound,
    is_connected,
#ifndef USE_BMC
    different_fairness,
#endif
    different_effect
  prove
    ass_detect_cycles;
#endif

#ifdef FORCE_ROOT_DET
forall (n in NODE) {
  nodes[n].force_root := 0;
}
#endif
#ifdef CONFIGURATION_DET
if (NUMNODES = 2) {
if (NUMPORTS = 3) {
  ass_userspec: assert F G 1;

  nodes[0].port[0].pnode := 1;
  nodes[0].port[0].pport := 0;
  init(nodes[0].port[0].role) := unknown;
  nodes[0].port[1].pnode := 0;
  nodes[0].port[1].pport := 0;
  init(nodes[0].port[1].role) := off;
  nodes[0].port[2].pnode := 0;
  nodes[0].port[2].pport := 0;
  init(nodes[0].port[2].role) := off;
  nodes[1].port[0].pnode := 0;
  nodes[1].port[0].pport := 0;
  init(nodes[1].port[0].role) := unknown;
  nodes[1].port[1].pnode := 0;
  nodes[1].port[1].pport := 0;
  init(nodes[1].port[1].role) := off;
  nodes[1].port[2].pnode := 0;
  nodes[1].port[2].pport := 0;
  init(nodes[1].port[2].role) := off;
}
}
if (NUMNODES = 3) {
if (NUMPORTS = 3) {
  ass_userspec: assert
  (~nodes[0].force_root &
  ~nodes[1].force_root &
  ~nodes[2].force_root) -> 
  F G nodes[1].is_root = 1;
  
  nodes[0].port[0].pnode := 1;
  nodes[0].port[0].pport := 0;
  init(nodes[0].port[0].role) := unknown;
  nodes[0].port[1].pnode := 0;
  nodes[0].port[1].pport := 0;
  init(nodes[0].port[1].role) := off;
  nodes[0].port[2].pnode := 0;
  nodes[0].port[2].pport := 0;
  init(nodes[0].port[2].role) := off;
  nodes[1].port[0].pnode := 0;
  nodes[1].port[0].pport := 0;
  init(nodes[1].port[0].role) := unknown;
  nodes[1].port[1].pnode := 2;
  nodes[1].port[1].pport := 0;
  init(nodes[1].port[1].role) := unknown;
  nodes[1].port[2].pnode := 0;
  nodes[1].port[2].pport := 0;
  init(nodes[1].port[2].role) := off;
  nodes[2].port[0].pnode := 1;
  nodes[2].port[0].pport := 1;
  init(nodes[2].port[0].role) := unknown;
  nodes[2].port[1].pnode := 0;
  nodes[2].port[1].pport := 0;
  init(nodes[2].port[1].role) := off;
  nodes[2].port[2].pnode := 0;
  nodes[2].port[2].pport := 0;
  init(nodes[2].port[2].role) := off;
}
}
if (NUMNODES = 5) {
if (NUMPORTS = 3) {
  ass_userspec: assert
  (~nodes[0].force_root &
  ~nodes[1].force_root &
  ~nodes[2].force_root &
  ~nodes[3].force_root &
  ~nodes[4].force_root) -> 
  F ((G nodes[1].is_root) | (G nodes[3].is_root));

  nodes[0].port[0].pnode := 1;
  nodes[0].port[0].pport := 0;
  init(nodes[0].port[0].role) := unknown;
  nodes[0].port[1].pnode := 0;
  nodes[0].port[1].pport := 0;
  init(nodes[0].port[1].role) := off;
  nodes[0].port[2].pnode := 0;
  nodes[0].port[2].pport := 0;
  init(nodes[0].port[2].role) := off;
  nodes[1].port[0].pnode := 0;
  nodes[1].port[0].pport := 0;
  init(nodes[1].port[0].role) := unknown;
  nodes[1].port[1].pnode := 3;
  nodes[1].port[1].pport := 0;
  init(nodes[1].port[1].role) := unknown;
  nodes[1].port[2].pnode := 0;
  nodes[1].port[2].pport := 0;
  init(nodes[1].port[2].role) := off;
  nodes[2].port[0].pnode := 0;
  nodes[2].port[0].pport := 0;
  init(nodes[2].port[0].role) := off;
  nodes[2].port[1].pnode := 3;
  nodes[2].port[1].pport := 1;
  init(nodes[2].port[1].role) := unknown;
  nodes[2].port[2].pnode := 0;
  nodes[2].port[2].pport := 0;
  init(nodes[2].port[2].role) := off;
  nodes[3].port[0].pnode := 1;
  nodes[3].port[0].pport := 1;
  init(nodes[3].port[0].role) := unknown;
  nodes[3].port[1].pnode := 2;
  nodes[3].port[1].pport := 1;
  init(nodes[3].port[1].role) := unknown;
  nodes[3].port[2].pnode := 4;
  nodes[3].port[2].pport := 0;
  init(nodes[3].port[2].role) := unknown;
  nodes[4].port[0].pnode := 3;
  nodes[4].port[0].pport := 2;
  init(nodes[4].port[0].role) := unknown;
  nodes[4].port[1].pnode := 0;
  nodes[4].port[1].pport := 0;
  init(nodes[4].port[1].role) := off;
  nodes[4].port[2].pnode := 0;
  nodes[4].port[2].pport := 0;
  init(nodes[4].port[2].role) := off;
}
}
if (NUMNODES = 6) {
if (NUMPORTS = 3) {
  ass_userspec: assert
  (~nodes[0].force_root &
  ~nodes[1].force_root &
  ~nodes[2].force_root &
  ~nodes[3].force_root &
  ~nodes[4].force_root) -> 
  F G nodes[3].is_root;
  
  nodes[0].port[0].pnode := 2;
  nodes[0].port[0].pport := 0;
  init(nodes[0].port[0].role) := unknown;
  nodes[0].port[1].pnode := 0;
  nodes[0].port[1].pport := 0;
  init(nodes[0].port[1].role) := off;
  nodes[0].port[2].pnode := 0;
  nodes[0].port[2].pport := 0;
  init(nodes[0].port[2].role) := off;
  nodes[1].port[0].pnode := 2;
  nodes[1].port[0].pport := 1;
  init(nodes[1].port[0].role) := unknown;
  nodes[1].port[1].pnode := 0;
  nodes[1].port[1].pport := 0;
  init(nodes[1].port[1].role) := off;
  nodes[1].port[2].pnode := 0;
  nodes[1].port[2].pport := 0;
  init(nodes[1].port[2].role) := off;
  nodes[2].port[0].pnode := 0;
  nodes[2].port[0].pport := 0;
  init(nodes[2].port[0].role) := unknown;
  nodes[2].port[1].pnode := 1;
  nodes[2].port[1].pport := 0;
  init(nodes[2].port[1].role) := unknown;
  nodes[2].port[2].pnode := 3;
  nodes[2].port[2].pport := 0;
  init(nodes[2].port[2].role) := unknown;
  nodes[3].port[0].pnode := 2;
  nodes[3].port[0].pport := 2;
  init(nodes[3].port[0].role) := unknown;
  nodes[3].port[1].pnode := 5;
  nodes[3].port[1].pport := 0;
  init(nodes[3].port[1].role) := unknown;
  nodes[3].port[2].pnode := 0;
  nodes[3].port[2].pport := 0;
  init(nodes[3].port[2].role) := off;
  nodes[4].port[0].pnode := 5;
  nodes[4].port[0].pport := 1;
  init(nodes[4].port[0].role) := unknown;
  nodes[4].port[1].pnode := 0;
  nodes[4].port[1].pport := 0;
  init(nodes[4].port[1].role) := off;
  nodes[4].port[2].pnode := 0;
  nodes[4].port[2].pport := 0;
  init(nodes[4].port[2].role) := off;
  nodes[5].port[0].pnode := 3;
  nodes[5].port[0].pport := 1;
  init(nodes[5].port[0].role) := unknown;
  nodes[5].port[1].pnode := 4;
  nodes[5].port[1].pport := 0;
  init(nodes[5].port[1].role) := unknown;
  nodes[5].port[2].pnode := 0;
  nodes[5].port[2].pport := 0;
  init(nodes[5].port[2].role) := off;
}
}
if (NUMNODES = 6) {
if (NUMPORTS = 4) {
  ass_userspec: assert F G 1;

  nodes[0].port[0].pnode := 2;
  nodes[0].port[0].pport := 0;
  init(nodes[0].port[0].role) := unknown;
  nodes[0].port[1].pnode := 0;
  nodes[0].port[1].pport := 0;
  init(nodes[0].port[1].role) := off;
  nodes[0].port[2].pnode := 0;
  nodes[0].port[2].pport := 0;
  init(nodes[0].port[2].role) := off;
  nodes[0].port[3].pnode := 0;
  nodes[0].port[3].pport := 0;
  init(nodes[0].port[3].role) := off;
  nodes[1].port[0].pnode := 2;
  nodes[1].port[0].pport := 1;
  init(nodes[1].port[0].role) := unknown;
  nodes[1].port[1].pnode := 0;
  nodes[1].port[1].pport := 0;
  init(nodes[1].port[1].role) := off;
  nodes[1].port[2].pnode := 0;
  nodes[1].port[2].pport := 0;
  init(nodes[1].port[2].role) := off;
  nodes[1].port[3].pnode := 0;
  nodes[1].port[3].pport := 0;
  init(nodes[1].port[3].role) := off;
  nodes[2].port[0].pnode := 0;
  nodes[2].port[0].pport := 0;
  init(nodes[2].port[0].role) := unknown;
  nodes[2].port[1].pnode := 1;
  nodes[2].port[1].pport := 0;
  init(nodes[2].port[1].role) := unknown;
  nodes[2].port[2].pnode := 3;
  nodes[2].port[2].pport := 0;
  init(nodes[2].port[2].role) := unknown;
  nodes[2].port[3].pnode := 4;
  nodes[2].port[3].pport := 1;
#ifdef SIX_NO_CYCLE
  init(nodes[2].port[3].role) := off; --unknown; --NOTE 4 1
#else
  init(nodes[2].port[3].role) := unknown;
#endif
  nodes[3].port[0].pnode := 2;
  nodes[3].port[0].pport := 2;
  init(nodes[3].port[0].role) := unknown;
  nodes[3].port[1].pnode := 5;
  nodes[3].port[1].pport := 0;
  init(nodes[3].port[1].role) := unknown;
  nodes[3].port[2].pnode := 0;
  nodes[3].port[2].pport := 0;
  init(nodes[3].port[2].role) := off;
  nodes[3].port[3].pnode := 0;
  nodes[3].port[3].pport := 0;
  init(nodes[3].port[3].role) := off;
  nodes[4].port[0].pnode := 5;
  nodes[4].port[0].pport := 1;
  init(nodes[4].port[0].role) := unknown;
  nodes[4].port[1].pnode := 2;
  nodes[4].port[1].pport := 3;
#ifdef SIX_NO_CYCLE
  init(nodes[4].port[1].role) := off; --unknown; --NOTE 2 3
#else
  init(nodes[4].port[1].role) := unknown;
#endif
  nodes[4].port[2].pnode := 0;
  nodes[4].port[2].pport := 0;
  init(nodes[4].port[2].role) := off;
  nodes[4].port[3].pnode := 0;
  nodes[4].port[3].pport := 0;
  init(nodes[4].port[3].role) := off;
  nodes[5].port[0].pnode := 3;
  nodes[5].port[0].pport := 1;
  init(nodes[5].port[0].role) := unknown;
  nodes[5].port[1].pnode := 4;
  nodes[5].port[1].pport := 0;
  init(nodes[5].port[1].role) := unknown;
  nodes[5].port[2].pnode := 0;
  nodes[5].port[2].pport := 0;
  init(nodes[5].port[2].role) := off;
  nodes[5].port[3].pnode := 0;
  nodes[5].port[3].pport := 0;
  init(nodes[5].port[3].role) := off;
}
}
if (NUMNODES = 10) {
if (NUMPORTS = 3) {
  ass_userspec: assert
  (~nodes[0].force_root &
  ~nodes[1].force_root &
  ~nodes[2].force_root &
  ~nodes[3].force_root &
  ~nodes[4].force_root &
  ~nodes[5].force_root &
  ~nodes[6].force_root &
  ~nodes[7].force_root &
  ~nodes[8].force_root &
  ~nodes[9].force_root) ->
  F ((G nodes[1].is_root) | (G nodes[3].is_root));

  nodes[0].port[0].pnode := 1;
  nodes[0].port[0].pport := 0;
  init(nodes[0].port[0].role) := unknown;
  nodes[0].port[1].pnode := 9;
  nodes[0].port[1].pport := 0;
  init(nodes[0].port[1].role) := unknown;
  nodes[0].port[2].pnode := 0;
  nodes[0].port[2].pport := 0;
  init(nodes[0].port[2].role) := off;
  nodes[1].port[0].pnode := 0;
  nodes[1].port[0].pport := 0;
  init(nodes[1].port[0].role) := unknown;
  nodes[1].port[1].pnode := 7;
  nodes[1].port[1].pport := 0;
  init(nodes[1].port[1].role) := unknown;
  nodes[1].port[2].pnode := 3;
  nodes[1].port[2].pport := 0;
  init(nodes[1].port[2].role) := unknown;
  nodes[2].port[0].pnode := 8;
  nodes[2].port[0].pport := 0;
  init(nodes[2].port[0].role) := unknown;
  nodes[2].port[1].pnode := 6;
  nodes[2].port[1].pport := 0;
  init(nodes[2].port[1].role) := unknown;
  nodes[2].port[2].pnode := 4;
  nodes[2].port[2].pport := 0;
  init(nodes[2].port[2].role) := unknown;
  nodes[3].port[0].pnode := 1;
  nodes[3].port[0].pport := 2;
  init(nodes[3].port[0].role) := unknown;
  nodes[3].port[1].pnode := 4;
  nodes[3].port[1].pport := 1;
  init(nodes[3].port[1].role) := unknown;
  nodes[3].port[2].pnode := 5;
  nodes[3].port[2].pport := 0;
  init(nodes[3].port[2].role) := unknown;
  nodes[4].port[0].pnode := 2;
  nodes[4].port[0].pport := 2;
  init(nodes[4].port[0].role) := unknown;
  nodes[4].port[1].pnode := 3;
  nodes[4].port[1].pport := 1;
  init(nodes[4].port[1].role) := unknown;
  nodes[4].port[2].pnode := 0;
  nodes[4].port[2].pport := 0;
  init(nodes[4].port[2].role) := off;
  nodes[5].port[0].pnode := 3;
  nodes[5].port[0].pport := 2;
  init(nodes[5].port[0].role) := unknown;
  nodes[5].port[1].pnode := 0;
  nodes[5].port[1].pport := 0;
  init(nodes[5].port[1].role) := off;
  nodes[5].port[2].pnode := 0;
  nodes[5].port[2].pport := 0;
  init(nodes[5].port[2].role) := off;
  nodes[6].port[0].pnode := 2;
  nodes[6].port[0].pport := 1;
  init(nodes[6].port[0].role) := unknown;
  nodes[6].port[1].pnode := 0;
  nodes[6].port[1].pport := 0;
  init(nodes[6].port[1].role) := off;
  nodes[6].port[2].pnode := 0;
  nodes[6].port[2].pport := 0;
  init(nodes[6].port[2].role) := off;
  nodes[7].port[0].pnode := 1;
  nodes[7].port[0].pport := 1;
  init(nodes[7].port[0].role) := unknown;
#if 1
  nodes[7].port[1].pnode := 0;
  nodes[7].port[1].pport := 0;
  init(nodes[7].port[1].role) := off;
#else
  nodes[7].port[1].pnode := 8;
  nodes[7].port[1].pport := 1;
  init(nodes[7].port[1].role) := unknown;
#endif
  nodes[7].port[2].pnode := 0;
  nodes[7].port[2].pport := 0;
  init(nodes[7].port[2].role) := off;
  nodes[8].port[0].pnode := 2;
  nodes[8].port[0].pport := 0;
  init(nodes[8].port[0].role) := unknown;
#if 1
  nodes[8].port[1].pnode := 0;
  nodes[8].port[1].pport := 0;
  init(nodes[8].port[1].role) := off;
#else
  nodes[8].port[1].pnode := 7;
  nodes[8].port[1].pport := 1;
  init(nodes[8].port[1].role) := unknown;
#endif
  nodes[8].port[2].pnode := 0;
  nodes[8].port[2].pport := 0;
  init(nodes[8].port[2].role) := off;
  nodes[9].port[0].pnode := 0;
  nodes[9].port[0].pport := 1;
  init(nodes[9].port[0].role) := unknown;
  nodes[9].port[1].pnode := 0;
  nodes[9].port[1].pport := 0;
  init(nodes[9].port[1].role) := off;
  nodes[9].port[2].pnode := 0;
  nodes[9].port[2].pport := 0;
  init(nodes[9].port[2].role) := off;
}
}
#endif

}
