Some Alloy programming pitfalls

• The next best thing to debugging, which you can't do in Alloy, is to  use the
• Be careful while using a predicate in an if condition, especially if the predicate body has an if condition 

          pred step(...) {
            ....
            r::next_sibling [n] implies {

            }
            ...
         }
         pred next_sibling(r:Run, n:Node)
          {
             let parent_nodes= r::nodes_at_level [r::prev_level[n] ]   |
               some parent_nodes implies
              {
                let siblings = parent_nodes.adjacency -  r::done_nodes[n] |
                  some siblings  implies
                    one m:siblings |
                            r::order[m] = r:: next_order[n]         
               }
            }
 This is completely wrong. I was mixing the imperative paradigm with Alloy's declarative one. But the following also doesn't quite work, because we are doing stuff in a predicate which is an if condition elsewhere. What we are doing may not be done if Alloy decides to have a false for the condition, while generating enumerations :-

         pred next_sibling(r:Run, n:Node)
          {
             let parent_nodes= r::nodes_at_level [r::prev_level[n] ]   |
               some parent_nodes and
              {
                let siblings = parent_nodes.adjacency -  r::done_nodes[n] |
                  some siblings  and
                   one m:siblings |
                            r::order[m] = r:: next_order[n]       
               }
            }

            
Best thing is to convert the predicates to functions which don't have any constraints if conditions (that may be set false by Alloy). What works is the following :-

pred step (r:Run, i : Order) {

     let n= r::node_at_order[i] | 

     {

       let sibs=r::next_siblings[n] |

        some sibs implies

        {

         one m:sibs | r::order[m] = r:: next_order[n]  and

           r::set_level[m,  r::level[n]] and

            r::set_done_nodes[m, r::done_nodes[n] + m ]

       }

      else

      {

         let  children=r::children_at_next_level[n] |

         some children implies

         {

           one m: children |

               r::order[m] = r::next_order[ n ] and

               r::set_level[m, r::next_level[n]]   and

               r::set_done_nodes[m, r::done_nodes[n]   + m]

        }

      }

.........

}

fun next_siblings(r:Run, n:Node): set Node

{

  let parent_nodes= r::nodes_at_level [r::prev_level[n] ]   |

     some parent_nodes implies

      {

       let siblings = parent_nodes.adjacency -  r::done_nodes[n] |

         some siblings  implies

            siblings      

         else

            none

     }

      else

            none

}

fun  children_at_next_level(r:Run, last_upper_node:Node) : set Node

{

    let n=last_upper_node |

           let peers= (r::nodes_at_same_level[n].adjacency - r::done_nodes[n]) |

           some peers implies

             peers

           else

             none

}