# Multi-Agent Systems with Information Sharing: Strategies and Model Checking
## 3 The Running Example Modeled by Using iMAS  
To illustrate the syntax and semantics of iMAS, let us describe in more detail the example mentioned in the introduction. A _student_ can use either a _bus_ or a _cab_ to move to a location (both _bus_ and _cab_ are encoded as agents). Additionally, the _student_ has to take into account a priority relation established between the transportation means: _cab_ is given a lower priority than _bus_. To make it easier to read the definitions of agents, we use the following notations: _WT_ (waiting time), _BAT_ (bus arrival time), _TT_ (travel time), _BC_ (bus capacity), _MBC_ (maximum bus capacity), _onB_ (get on the bus), _offB_ (get off the bus), _schd_ (waiting according to the schedule), _wait_ (student is waiting), and _STT_ (student travel time). Similar notations are used for _bus_ and _student_ when they are in _home_. The _bus_ at location \(l\) having the destination \(l^{\prime}\) can be described as  
\(bus(l,l^{\prime})=\mathit{offB}^{\Delta 0}\gamma(x_{1})\) then \(upd(private,BC,get(private,BC)-1)\) then \(bus(l,l^{\prime})\)  
else if \(get(private,BC)<get(private,MBC)\)  
then \(onB^{\Delta 0}\{get(private,TT(l,l^{\prime}))\}\)  
then \(upd(private,BC,get(private,BC)+1)\)  
then \(bus(l,l^{\prime})\)  
else \(go^{get(private,TT(l^{\prime}))}\)\(l^{\prime}\) then \(bus(l^{\prime},l)\)  
else \(go^{get(private,TT(l^{\prime}))}\)\(home\) then \(bus(l^{\prime},l)\). The passengers are allowed to go off the _bus_ by using a channel _offB_, and this is followed by a decrease in the number of passengers in the _bus_. Afterwards, any passengers willing to travel by _bus_ communicate on the channel _onB_ to receive the travel time from the field \(TT(l,l^{\prime})\) of the _private_ information of the _bus_, and this is followed by an increase in the number of passengers in the _bus_. Once the _bus_ took all the passengers, it moves to the location \(l^{\prime}\). Similarly, a _cab_ at the location \(l\) can be described as  
\(\mathit{cab}(l)=\mathit{onC}^{\infty}? (x_{2})\) then \(\mathit{onC}^{\Delta 0}! (\mathit{get}(\mathit{private},TT(l,x_{2})))\)  
\(\mathit{then}\ \mathit{go}^{\mathit{gt}(\mathit{private},TT(l,x_{2}))}\ x_{2}\) then \(\mathit{offC}^{\infty}? (x_{3})\) then \(\mathit{cab}(x_{2})\)  
\(\mathsf{else}\ \mathit{cab}(l)\)  
\(\mathsf{else}\ \mathit{stop}\)  
\(\mathsf{else}\ \mathit{stop}\). The _cab_ awaits for a location to be communicated by the _student_ on the channel _onC_; once it receives this location, it sends back the travel time between the current location and the desired one. Afterwards, the _cab_ moves to the \(l^{\prime}\) location, where the _student_ can exit the _cab_. The description of the _student_ at the location \(l\) having the destination \(l^{\prime}\) is as follows:  
\(\mathit{student}(l,l^{\prime})=\mathsf{if}\ \mathit{get}(\mathit{public},\mathit{BAT })<\mathit{get}(\mathit{private},\mathit{WT}(l))\)  
\(\mathsf{then}\ \mathit{onB}^{\mathit{Agent}(\mathit{private},\mathit{WT}(l))}? (x_{4})\)  
\(\mathsf{then}\ \mathit{upd}(\mathit{private},\mathit{STT},x_{4})\) then \(\mathit{go}^{\mathit{gt}(\mathit{private},\mathit{STT})}\ l^{\prime}\)  
\(\mathsf{then}\ \mathit{offB}^{\Delta 0}! (x_{4})\)  
\(\mathsf{then}\ \mathit{wait}^{\mathit{Agret}(\mathit{private},\mathit{WT}(l))}! (x_{4})\)  
\(\mathsf{then}\ \mathit{stop}\ \mathsf{else}\ \mathit{student}(l^{\prime},l)\)  
\(\mathsf{else}\ \mathit{stop}\)  
\(\mathsf{else}\ \mathit{student}(l,l^{\prime})\). If the _bus_ and the _student_ are in the same time at the same location, then they can communicate using the channel _onB_. If however, the _bus_ and the _student_ are not in the same time at the same location, and it takes longer for the _bus_ to arrive than the _student_ is willing to wait, then the _student_ will try to find a _cab_ to reach their destination. If the _student_ and the _cab_ are at the same location, then they can communicate using the channel _onC_.