/*
NAME
  Crossing a bridge in the dark (LTL version)

SYNOPSIS
  run under the SLIM LTL mode
  property: not everybody can cross the bridge in 17 minutes
  
AUTHOR
  Ryo Okabe

HISTORY
  2008/01/31(Thu)
*/

x(0,1), x(0,2), x(0,5), x(0,10), light(0),total(0).

go@@
x(0,T1), x(0,T2), total(S), light(0) :- T1>=T2, S2=S+T1 |
  x(1,T1), x(1,T2), total(S2), light(1).

back@@
x(1,T), total(S), light(1) :- S2=S+T |
  x(0,T), total(S2), light(0).
