hallway.als

module hallway
open util/ordering[Time]

sig Time {}

abstract sig Position {}
one sig Left, Right, Passed extends Position {}

abstract sig Person {
  position: Position one -> Time
}

fun dodgePos: set Position {
	Left + Right
}

one sig Me, You extends Person {}

pred init (t: Time) {
	all p: Person | p.position.t in dodgePos
}

pred dodge (t, t': Time, p: Person) {
    all d: Person | d.position.t in dodgePos
	some pos: dodgePos | p.position.t' = pos
}

pred pass (t, t': Time, p: Person) {
    all d: Person | (d.position.t = p.position.t) => (d = p)
	(Person - p).position.t = Passed => p.position.t' != Passed
	p.position.t' = Passed
}

fact Traces {
	first.init
	all t: Time - last | let t' = t.next |
		all p: Person {
			dodge [t, t', p] or pass [t, t', p]
		}
}

pred show {}
run show 

pred awkwardnessEnds {
	some t: Time | some p: Person | p.position.t = Passed
}

assert cleanPass {
	all t: Time - last | let t' = t.next |
		some p: Person | p.position.t' = Passed => Me.position.t != You.position.t
}

check cleanPass 
run awkwardnessEnds