Building-Gate model

Alloy 6
1

I am trying to model a Building-Gate model, initially in the building no gate (open or closed) should be present, then for after traces newgate or disablegate can be used to open a new gate(status:open) or disable an existing one(status:closed). But running example predicate returns with no instances. What is the best way to model this or where am I making a mistake?

 enum Status{OPEN, CLOSED}

sig Gate{
	var status : Status
}

one sig Building{
	var gates : disj set Gate,
	var disabled : disj set Gate
}

pred newgate [g : Gate]{
	gates' = gates + Building->g
	status' = status + g->OPEN
	disabled' = disabled
}

pred disablegate [g: Gate]{
	g in Building.gates
	status' = (status - g->OPEN) + g->CLOSED
	gates' = gates - Building->g
	disabled' = disabled + Building->g
}
fact init {
	no gates
	no disabled
}

fact trans {

	always (some g : Gate | newgate[g] or disablegate[g])	
	always status.OPEN = Building.gates
	always status.CLOSED = Building.disabled
}

run example {eventually no status.OPEN} for 5

assert newgate_after_close {
  always (all g : Gate | disablegate[g] implies once newgate[g])
}
check newgate_after_close
2

After a quick look, it seems to me the error is the following:

  • In init, you’re saying that gates and disabled are empty.
  • But then (in trans) status.OPEN is specified to be always equal to Building.gates, hence empty in the first instant. Similarly for status.CLOSED.
  • But every gate is either open or closed. Therefore Gate is empty in the first state. As Gate is static (= non-var), it is always empty.
  • Therefore, no trace can satisfy some g: Gate | ... in trans: the specification is inconsistent.

Two remarks:

  • the disj in the definitions of gates and disabled say that each of these relations is injective, that is two different buildings have disjoint gates, but as there’s only one building… If you wanted to say that gates and disabled are always disjoint, then you should rather write disj gates, disabled: set Gate. Most of the time, I think this is unadvised: instead of enforcing such an implicit fact, you should rather check that this is implied by the events.
  • The last two statements in trans are, similarly, dangerous (as was particularly witnessed here). Once again, in general, most properties should rather be checked than enforced.
3

thank you very much for your comments. It made some progress, but I couldn’t make the gates always belong to the Building… The code that is commented in the trans

enum Status{OPEN, CLOSED}

var sig Gate{
	var status : lone Status
}

var one sig Building{
	var gates : disj set Gate,
	var disabled : set Gate
}

pred newgate [g : Gate]{
	gates' = gates + Building->g
	status' = status + g->OPEN
	disabled' = disabled
}

pred disablegate [g: Gate]{
	g in Building.gates
	status' = (status - g->OPEN) + g->CLOSED
	gates' = gates - Building->g
	disabled' = disabled + Building->g
}
fact init {
	no gates
	no disabled
}

fact trans {
	always (some g : Gate | newgate[g] or disablegate[g])	
--	always (all g : Gate | g in Building.gates or g in Building.disabled )
}

run example {#status.OPEN>1} for 5
4

Are you trying to specify a fictitious worlds where there is exactly one building to which you may add open gates, which can then be closed? If so, I think there’s no reason for Building nor Gate to be var.

You had left a disj in the gates but once again, it’s of no use if there’s only one building.

Also observe the use of ++ in disablegate which makes the specification more readable.

Unless I’m mistaken, the way you wrote your events prevented the existence of an infinite trace (because you cannot indefinitely add and disable gates and there’s only a finite supply of Gates).

However Alloy does not consider finite traces at all. All traces must be infinite, which is one of the reasons to add a skip event (this way, instead of a “forbidden” finite trace, you can end up with an infinite trace doing skip indefinitely in the last state).

enum Status{OPEN, CLOSED}

sig Gate{
	var status : one Status
}

one sig Building{
	var gates : set Gate,
	var disabled : set Gate
}

pred newgate [g : Gate]{
	g not in Building.gates
	gates' = gates + Building->g
	status' = status + g->OPEN
	disabled' = disabled
}

pred disablegate [g: Gate]{
	g in Building.gates
	status' = status ++ g->CLOSED
	gates' = gates - Building->g
	disabled' = disabled + Building->g
}

let unchanged[r] { r = (r)' }

pred skip {
	unchanged[status]
	unchanged[gates]
	unchanged[disabled]
}

fact init {
	no gates
	no disabled
}

fact trans {
	always (skip or some g : Gate | newgate[g] or disablegate[g])	
}

run example {} for 5
5

Thank you very much for your help, that’s exactly what I wanted