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"

}