//This file was generated from UPPAAL2k.

/*
Four vikings are about to cross a damaged bridge in the middle of the
night. The bridge can only carry two of the vikings at the time and to
find the way over the bridge the vikings need to bring a torch.  The
vikings need 5, 10, 20 and 25 minutes (one-way) respectively to cross
the bridge.

Does a schedule exist which gets all four vikings over the bridge
within 60 minutes?
*/
//NO_QUERY


/*
Viking 1 can cross the bridge.
*/
E<>( Viking1.safe )


/*

*/
E<>( Viking2.safe )


/*

*/
E<>( Viking3.safe )


/*

*/
E<>( Viking4.safe and time<slowest )


/*

*/
E<>( Viking4.safe and time<=slowest )


/*
Scheduling problem reformulated as reachability property.
*/
E<>( Viking1.safe and Viking2.safe and Viking3.safe and Viking4.safe and time <= 60 )