INHERIT system  --  defines software_system, proposed.

--  controls

INHERIT user  --  defines User_class, uses

INHERIT business  --  defines vendor, customer, sells

IMPORT Subtype FROM type

CONCEPT airline_reservation_system: software_system

  WHERE proposed (airline_reservation_system),

        --We are going to build an airline reservation

-- system

     Controls (airline_reservation_system, reservation)

       --The system will help travel agents sell tickets by

       --managing reservations.

CONCEPT travel_agent: User_class

  WHERE ALL(ta: travel_agent

::uses(ta, airline_reservation_system)),

        --Travel agents use the airline reservation system.

        --We are only concerned with the travel agents using

        --our system.

Subtype(travel_agent, vendor),

--A travel agent is a sales person.

ALL(t : ticket :: SOME (ta: travel_agent

:: sells(ta, t) )),

    ALL(r: reservation :: SOME (ta: travel_agent

      :: supplies(ta, t) ))

--Travel agents are the only sources for tickets

--and reservations.

CONCEPT ticket: type

   WHERE Subtype(ticket, product),

      ALL (t: trip :: Needed_for(ticket, t))

--A ticket is needed for every trip.

CONCEPT trip : type

   WHERE Subtype (trip, activity),

      ALL(t: trip :: Needed_for (flight, t))

--A flight is needed for every trip.

CONCEPT passenger : type

WHERE Subtype (passenger ,custom),

      ALL (p: passenger :: SOME(t: trip :: wants(p, t))),

ALL (p: passenger :: SOME(t: ticket :: buys(p, t)))

CONCEPT airline : type

WHERE Subtype(airline, supplier),

      ALL(f: flight :: SOME(a: airline :: supplies(a, f)))

        --Every flight is associated with an airline.

        --We are only concerned with commercial flights.

CONCEPT flight :type

WHERE Subtype(flight, activity)

CONCEPT reservation : type

WHERE ALL (t: trip :: SOME(r: reservation

 :: Neded_for (r, t)))