// jeh 27/2/07
// Web service composition example, with sessions and validity checking
// for the Bertinoro book chapter

/* Model modified. Stateless PAProvider and Customer added --mtribast */

r1 = 0.001;
r2 = 0.5;
r3 = 0.1;
r4 = 0.1;
r5 = 0.05;
r6 = 0.1;
r7 = 0.05;
r8 = 0.02;
r9 = 0.2;

Customer = (getSMS, r1).Customer1;
Customer1 = (getMap, infty).Customer + (get404, infty).Customer;

WSConsumer = (notify, infty).WSConsumer2;
WSConsumer2 = (locRequest, r4).WSConsumer3;
WSConsumer3 = (locResult, infty).WSConsumer4
            + (locError, infty).WSConsumer;
WSConsumer4 = (compute, r7).WSConsumer5;
WSConsumer5 = (sendMMS, r9).WSConsumer;

WSProvider = (getSMS, infty).WSProvider2;
WSProvider2 = (startSession, r2).WSProvider3;
WSProvider3 = (notify, r3).WSProvider4;
WSProvider4 = (locRequest, infty).WSProvider5;
WSProvider5 = (checkValidity, 99*infty).WSProvider6
            + (checkValidity, infty).WSProvider10;
WSProvider6 = (locResult, r6).WSProvider7;
WSProvider7 = (sendMMS, infty).WSProvider8;
WSProvider8 = (getMap, r8).WSProvider9;
WSProvider9 = (stopSession, r2).WSProvider;
WSProvider10 = (locError, r6).WSProvider11;
WSProvider11 = (get404, r8).WSProvider9;

 /*State-less provider */
PAProvider = (startSession, infty).PAProvider +
       (checkValidity, r5).PAProvider +
       (stopSession, infty).PAProvider;

 /* Stateful Provider */
/*PAProvider =  (startSession, infty).PAProvider1;
PAProvider1 = (checkValidity, r5).PAProvider2;
PAProvider2 = (stopSession, infty).PAProvider;*/

Customer[1] <getSMS, getMap, get404>
       ((WSProvider[1] <notify,locRequest,locResult,locError,sendMMS>
               WSConsumer[1]) <startSession,checkValidity,stopSession> PAProvider[1])