open util/ordering[State]

sig State {
	marcacao : set Lugar
}

abstract sig No {}

sig Lugar extends No {
	pre : set Accao
}

sig Init in Lugar {}

sig Accao extends No {
	pos : set Lugar
}

fun flow : No -> No {
	pre + pos
}

pred activa [a : Accao, s : State] {
	flow.a in s.marcacao
	no a.flow & (s.marcacao - flow.a)
}

pred dispara [a : Accao, s,s' : State] {
	activa[a,s]
	s'.marcacao = s.marcacao - flow.a + a.flow
}

pred nop [s,s' : State] {
	no a : Accao | activa[a,s]
	s'.marcacao = s.marcacao
}

fact {
	first.marcacao = Init
	all s : State - last {
		(some a : Accao | dispara[a,s,s.next]) or 
		nop [s,s.next]
	}
}

run {} for 3 but 10 State