How to make a pred initialevent based on case study

Questions
1

–ACME TRAVEL PROHIBIT R6,7,8,11,12,37
–a set of participant
–23/11/2023
–no inclusive OR over participants/events, no static and date constraints
–prohibition applied, XOR applied
–still no intstance found even after remove the prohibition (pred initialevent)

module ATcasestudy

abstract sig participant {}
one sig customer extends participant{sends:one reservationrequest, receives: one notification}
one sig AT extends participant{receives: one reservationrequest, requestfor: one reservation, sends: one notification}
one sig airline extends participant{receives: one reservation, sends: one airlineresponse}
one sig touragency extends participant{receives: one reservation, sends: one tourresponse} 
--receives4: lone accomreservation, receives5: lone transreservation}
--{#receives4 =0 and #receives5=0} --prohibit rule 8
abstract sig accommodation extends participant{sends: one accomresponse}
	{(accommodation= hotel and no apartment) or (accommodation=apartment and no hotel )}
	lone sig hotel extends accommodation {receives: one hotelreservation}--, receives2: lone apartmentreservation}
	--{#receives2 =0}--prohibit rule 6
	lone  sig apartment extends accommodation {receives: one apartmentreservation}--, receives3: lone hotelreservation}
	--{#receives3 =0}--prohibit rule 7 
abstract sig transport extends participant{sends: one transresponse}
	{(transport= bus and no train) or (transport=train and no bus )}
	lone sig bus extends transport {receives: one busreservation}
	lone sig train extends transport {receives: one trainreservation}

-----------------------event set------------------------

abstract sig event {}

one sig reservationrequest extends event{immediatelyprecedes: one reservation, at1: one T1_RR,at2: one T2_RR}
{immediatelyprecedes=AT.requestfor and immediatelyprecedes=airline.receives and immediatelyprecedes=touragency.receives}

abstract sig reservation extends event{at1: one T1_R,at2: one T2_R}
{(reservation=airlinereservation and no tourreservation and no accomreservation and no transreservation) or
(reservation=transreservation and no airlinereservation and no accomreservation and no tourreservation) or
(reservation=accomreservation and no tourreservation and no airlinereservation and no transreservation) or
(reservation=tourreservation and no airlinereservation and no accomreservation and no transreservation)}
	lone sig airlinereservation extends reservation {immediatelyprecedes: one airlineresponse}
	{immediatelyprecedes = airline.sends} 
	lone sig tourreservation extends reservation{immediatelyprecedes: one tourresponse}
	{immediatelyprecedes = touragency.sends}
	lone sig accomreservation extends reservation {immediatelyprecedes: one accomresponse}
		{(accomreservation= hotelreservation and no apartmentreservation) or 
		(accomreservation=apartmentreservation and no hotelreservation ) and (immediatelyprecedes =accommodation.sends)}
		lone sig hotelreservation extends accomreservation{}
		lone sig apartmentreservation extends accomreservation{}
	lone sig transreservation extends reservation{immediatelyprecedes: one transresponse} 
		{(transreservation= busreservation and no trainreservation) or 
		(transreservation=trainreservation and no busreservation ) and (immediatelyprecedes = transport.sends)} 
		lone sig busreservation extends transreservation{}
		lone sig trainreservation extends transreservation{}

abstract sig airlineresponse extends event {immediatelyprecedes: one notification,-- immediatelyprecedes1: lone airlinereservation,
at1: one T1_ARR,at2: one T2_ARR }
{(airlineresponse= succairline and no unsuccairline) or (airlineresponse = unsuccairline and no succairline) 
and immediatelyprecedes = AT.sends and immediatelyprecedes = customer.receives }--and #immediatelyprecedes1 = 0}--prohibit rule 11
	lone sig succairline extends airlineresponse{}
	lone sig unsuccairline extends airlineresponse{}

abstract sig accomresponse extends event {immediatelyprecedes: one notification, --immediatelyprecedes2: lone accomreservation, 
at1: one T1_ACR,at2: one T2_ACR }
{(accomresponse= succaccom and no unsuccaccom) or (accomresponse = unsuccaccom and no succaccom)
and immediatelyprecedes = AT.sends and immediatelyprecedes = customer.receives }
--and #immediatelyprecedes2 =0}--prohibit rule 12
	lone sig succaccom extends accomresponse{}
	lone sig unsuccaccom extends accomresponse{}

abstract sig tourresponse extends event{immediatelyprecedes: one notification, at1: one T1_TRR,at2: one T2_TRR }
{(tourresponse= succatour and no unsucctour) or (tourresponse = unsucctour and no succatour)
and immediatelyprecedes = AT.sends and immediatelyprecedes = customer.receives}
	lone sig succatour extends tourresponse{}
	lone sig unsucctour extends tourresponse{}

abstract sig transresponse extends event {immediatelyprecedes: one notification, at1: one T1_TPR,at2: one T2_TPR}
{(transresponse= succatransres and no unsucctransres) or (transresponse = unsucctransres and no succatransres)
and immediatelyprecedes = AT.sends and immediatelyprecedes = customer.receives}
	lone sig succatransres extends transresponse{}
	lone sig unsucctransres extends transresponse{}

--PROHIBIT RULE 39
one sig notification extends event{}--immediatelyprecedes3:lone accomresponse, immediatelyprecedes4:lone tourresponse,
--immediatelyprecedes5:lone transresponse, immediatelyprecedes6:lone airlineresponse, at: one T1_N, at1: one T2_N}
--{#immediatelyprecedes3 =0  and #immediatelyprecedes4 =0   and #immediatelyprecedes5 =0  
--and #immediatelyprecedes6 =0  }

---------------------time------------------------------

abstract sig time{}

abstract sig reservationrequest_time extends time{}
one sig T1_RR extends reservationrequest_time { by:one customer, immediatelyprecedes: one T2_RR}
one sig T2_RR extends reservationrequest_time { by:one AT} 

abstract sig reservation_time extends time{}
one sig T1_R extends reservation_time { by:one AT, immediatelyprecedes: one T2_R}
one sig T2_R extends reservation_time { by1:one airline, by2: one touragency} 

abstract sig airlineresponse_time extends time{}
one sig T1_ARR extends airlineresponse_time { by:one airline, immediatelyprecedes: one T2_ARR}
one sig T2_ARR extends airlineresponse_time { by:one AT}

abstract sig aaccomresponse_time extends time{}
one sig T1_ACR extends aaccomresponse_time { by:one accommodation, immediatelyprecedes: one T2_ACR}
one sig T2_ACR extends aaccomresponse_time { by:one AT}

abstract sig tourresponse_time extends time{}
one sig T1_TRR extends tourresponse_time { by:one touragency, immediatelyprecedes: one T2_TRR}
one sig T2_TRR extends tourresponse_time { by:one AT}

abstract sig transresponse_time extends time{}
one sig T1_TPR extends transresponse_time { by:one AT, immediatelyprecedes: one T2_TPR}
one sig T2_TPR extends transresponse_time { by:one customer}

abstract sig notification_time extends time{}
one sig T1_N extends notification_time { by:one AT, immediatelyprecedes: one T2_N}
one sig T2_N extends notification_time { by:one customer}

-- predicates for generating the SBVR Model
pred initialevent[r: reservationrequest, a: airlinereservation, c: accomreservation, t: tourreservation, s: transreservation] 
{(r.immediatelyprecedes= a and r.immediatelyprecedes!= c and r.immediatelyprecedes!= t and r.immediatelyprecedes!= s)}
run initialevent for 1 reservationrequest, 1 airlinereservation, 1 accomreservation, 1 tourreservation, 1 transreservation

pred initalevent2[ r:reservationrequest, a:airlinereservation, c: accomreservation,  t:tourreservation, s: transreservation]
{(r.immediatelyprecedes= a and r.immediatelyprecedes!= c and r.immediatelyprecedes!= t and r.immediatelyprecedes!= s) or
(r.immediatelyprecedes= c and r.immediatelyprecedes!= a and r.immediatelyprecedes!= t and r.immediatelyprecedes!= s) or
(r.immediatelyprecedes= t and r.immediatelyprecedes!= c and r.immediatelyprecedes!= a and r.immediatelyprecedes!= s) or
(r.immediatelyprecedes= s and r.immediatelyprecedes!= c and r.immediatelyprecedes!= t and r.immediatelyprecedes!= a) }
run initalevent2

--verifying the SBVR model
pred concreterequest[p:airline, e:succairline] 
{p.sends = e}
run concreterequest

pred showATcasestudy{}
run showATcasestudy

the rule is: it is obligatory that exactly one reservation request immediately precedes exactly one reservation that includes exactly one airlinereservation or exactly one accomreservation or exactly one tourreservation or exactly one transreservation, but not all

based on the rule, reservation request is the initial event.

my concern is, why i cant show (instance) for the pred initialevent? (as shown in the Alloy snipper) and how to show the pred initial event in the right way?

2

Hi,
To find an instance of the predicate initialevent you need at least one atom for each of the parameters. However, you have a signature fact in the reservation signature requiring that if the reservation is an airline reservation then the other kinds of reservations cannot exist, so it is impossible to instantiate the predicate.
Best,
Alcino

3

Hi,

Thank you for your response.

Then, in your opinion, how can I correct this?

4

It is difficult to suggest something, because I don’t know what are you trying to model, and the model you sent is quite complex.
Sorry,
Alcino

1 Like