How to model a toggle-able graph network? — Part 1

The road ends at formal software design with Alloy. And teaches me the expressive language of set theory.

What is a toggle-able graph network?

The node is able to be hidden or expanded following some criterion.

Potential cases

Different criterion would lead to different behaviors.

• case 1

• case 2

How to check your criterion?

Since multiple criterion are acceptable, the key point is not to find the unique solution, instead, to find the criterion of the criterion, that is, to check the consistency and validity of the criterion.

For example,

1. Is the node state deterministic?
2. Is the definitions of node state complete?

So the next question is, which language is suitable to articulate the problem and then to look for solution?

Natural language vs. formal language

• Natural language

From observation, we can summarize the criterion in case 1 are,

a). If a selected node is a fully expanded node, then it becomes a toggled node.

b). If a selected node is NOT a fully expanded node, then it becomes a fully expanded node.

c). A toggled node is a node whose inbounded nodes and all their inbounded nodes are all hidden nodes.

d). A fully expanded node is a node whose directly connected nodes are all visible (no hidden nodes).

• Formal language using Alloy syntax

sig Node {
  ,to : lone Node
  ,var nodeState : NodeState
}
var lone sig SelectedNode in Node {}

abstract sig NodeState {}
one sig FullyExpanded, Toggled, Hidden extends NodeState {}

pred handleSelectedNode[selectedNode : SelectedNode]{
  selectedNode.nodeState in FullyExpanded => {
    selectedNode.nodeState' in Toggled 
  }
  else {
    selectedNode.nodeState' in FullyExpanded
  }
  #(SelectedNode') = 0
}

pred ToggledNodeFact {
  all node : Node | node.nodeState in Toggled => node.^(~to).nodeState in Hidden
}
pred FullyExpandedNodeFact {
  all node : Node | node.nodeState in FullyExpanded => {
    (node.to.nodeState + node.(~to).nodeState ) in (NodeState - Hidden)
  }
}

fact {
  always (ToggledNodeFact and FullyExpandedNodeFact)
}

run {
  one SelectedNode
  handleSelectedNode[SelectedNode]
} for 3

What is Alloy?

Alloy is an open source language and analyzer for software modeling.

You can have an overview from Alloy’s official website.

There some books and online documents of Alloy.

I find courses on Alloy provides a good starting point to learn Alloy.

Among them, I had read through slides in CS:5810 Formal Methods in Software Engineering, University of Iowa. The latest version is Fall 2023.

It explains very well the root of Alloy is in set theory. Many of the terminology in Alloy would be better understood if you understand it in the context of set theory.

For example,

• A relation is a tuple.
• A function is a relational function which returns a relation.

The deficit of natural language

Are the criterion we wrote down based on observation good enough? We can not tell by naked eye.

However, using Alloy, we can quickly spot some deficits in our criterion.

• Deficit 1: Can a hidden node have a toggled node as inbound node? We does not cover it in our criterion.

• Deficit 2: Can a node reference to itself? We does not cover it in our criterion.

• Deficit 3: If there is no inbound node, is the node still a toggled node? We does not cover it in our criterion.

Even if we could enumerate, enumeration is still not enough to do model checking. We need some formal methods. In next part, I will introduce formal methods in Alloy for model checking.