module Label

sig Item {
	var labels : set Label
}
sig Label {}

// Actions

pred affix [i : Item, l : Label] {
  	// guard
  	l not in i.labels
  	// effect
  	i.labels' = i.labels + l
  	// frame condition
  	all j : Item - i | j.labels' = j.labels
}

pred detach [i : Item, l : Label] {
  // guard
  l in i.labels
  // effect
  labels' = labels - i->l
}

pred clear [i : Item] {
  // guard
  some i.labels
  // effect
  labels' = labels - i->Label
}

pred stutter {
	labels' = labels
}

// Behavior

fact Behavior {
  	no labels
  	always {
    	(some i : Item, l : Label | affix[i,l] or detach[i,l])
    	or 
    	(some i : Item | clear[i])
    	or
    	stutter 
  	}
}

// Scenarios

run Scenario1 {
  	some i : Item, disj l,m : Label {
    	affix[i,l]; affix[i,m]; clear[i]
  	}
} expect 1

run Scenario2 {
  	some i : Item, l : Label {
    	affix[i,l]; affix[i,l]
  	}
} expect 0