argument: LocLog2
A1 "Current location of <<user>> is logged 
    when 'update' action is performed by <<the user>>" 
   with IsPerformedBy(updateAction, User, t) -> IsLoggedIn(Location, User, Storage, t+4) {
	supported by
		F2 "The GPS unit always gives 
		    the current location accurately" with IsAccurate(GPS_Unit, Location)
		F1 "The device interface never 
		    indicates to the machine that 
		    <<the user>> has given the 'update'
		    instruction when <<the user>> has not" with 
IsPerforming(User, updateAction, t) -> Indicates(Device_Interface, Location_Logger, updateAction, t + 1)
		F3 "The Wifi connection never 
		    fails to relay the log entry" with
Transmission(WifiConnection, Location, User, t) -> IsLoggedIn(Location, User, Storage, t+1)
		F4 "<<The user>> wants precise
		    location to be recorded when abroad" with
IsAbroad(User, t) & IsLogged(Location, User, Storage, t) -> IsAccurate(Location, t)
		F5 "Sarah is a user and she is abroad" with IsAbroad(sarah) & IsA (sarah, User) 
		F6 "Adam is a user and he is not abroad" with ! IsAbroad(adam) & IsA (adam, User) 
	warranted by
		W1 "!F4 -> !A1"
}