//This file was generated from UPPAAL 4.1.0 (rev. 3323), November 2007 /* Is it possible for the first cryptographer to roll 0 (tails)? */ E<> Waiter.RolledTheCoin and answer[0]==0 /* Is it possible for the first cryptographer to roll 1 (heads?)? */ E<> Waiter.RolledTheCoin and answer[0]==1 /* If agency paid then the agencyPaid variable is true, if agency did not pay then the agencyPaid is false. */ A[] Waiter.done imply ((Agency.Paid && agencyPaid) or (!Agency.Paid && !agencyPaid)) /* If agency did not pay, then some cryptographer has announced that he paid. */ A[] Waiter.done imply (not agencyPaid imply exists(id: id_t) Crypt(id).Paid) /* If agency paid, then no cryptographer has announced that he paid. */ A[] Waiter.done imply (agencyPaid imply not exists(id: id_t) Crypt(id).Paid)