I have to realize an application which permits to reserve a seat in a store. There are no sintax error, but I don't understand why terminal reply me "predicate not consistent". Can u help me? This is my code:
open util/integer
sig Email{}
sig CF{}
sig Time{
hour: one Int,
minute:one Int,
second: one Int
}
abstract sig RegisteredUser{
email: one Email
}
sig User extends RegisteredUser{
cf: one CF
}
sig SM extends RegisteredUser{
cf: one CF,
store: one Store
}
sig Location{}
sig Date{}
abstract sig Status {}
//only one of this can be true
one sig Waiting extends Status {}
one sig Expired extends Status{}
one sig Pending extends Status{}
sig Ticket{
owner:one User,
date: one Date,
time: one Time,
status : one Status,
}
sig Visit{
owner:one User,
date: one Date,
time: one Time,
duration:one Time,
status : one Status,
products: some Product,
category: some Category,
}
//tickets are assumed with a default duration time of 15 min and entrance one for time, so 4*8=32 visit per day
sig TicketQueue {
max_visit:one Int,
ticket: some Ticket,
manager: one SM
}
sig VisitQueue{
category: some Category,
visit: some Visit,
manager: one SM
}
sig Store{
max_simultaneous: one Int,
location: one Location,
visitqueue: one VisitQueue,
ticketqueue: one TicketQueue,
product_category: some Category
}
sig Category{
simultaneous_seats: one Int,
}
sig Product{
category: one Category
}
// Constraints
// Registration data for the system are unique(Unique username and Fiscal Code)
fact registrationDataUniqueness {
no disjoint u1, u2: RegisteredUser | u1.email = u2.email
no disjoint u1,u2: User | u1.cf = u2.cf
no disjoint s1,s2: SM | s1.cf = s2.cf
no disjoint s:SM, u:User | s.cf=u.cf
}
//Ticket and Visit can have only one of status' values defined before
fact requestConsistency {
all s: Status | (s = Waiting && s != Expired && s !=Pending ) || (s != Waiting && s = Expired && s != Pending) || (s !=Waiting && s != Expired && s = Pending)
}
//SM can manage only one Store
fact StoreUniqueness{
no disjoint s1,s2: SM |s1.store=s2.store
}
// the same ticket or visit cannot be of two or more different user
fact UserUniqueness{
no disjoint t1,t2: Ticket | t1.owner=t2.owner
no disjoint v1,v2: Visit | v1.owner=v2.owner
}
//different products can not be of the same category
fact CategoryUniqueness{
no disjoint p1,p2: Product | p1.category=p2.category
}
//different stores can't have the same ticket or visit queue
fact QueueUniqueness{
no disjoint s1,s2: Store | s1.ticketqueue=s2.ticketqueue
no disjoint s1,s2: Store | s1.visitqueue=s2.visitqueue
}
//different tickets cannot have the same time
fact TimeUniqueness{
no disjoint t1,t2: Ticket | t1.time = t2.time
}
//for semplicity,in the visit/ticket queue, we consider "active" only visit/ticket with Waiting status
fact StatusQueue{
all tq:TicketQueue | tq.ticket.status=Waiting
all vq:VisitQueue | vq.visit.status=Waiting
}
//one ticket/visit can not belong to two or more different queue
fact ReservationUniqueness{
no disjoint tq1,tq2:TicketQueue | tq1.ticket=tq2.ticket
no disjoint vq1,vq2:VisitQueue | vq1.visit=vq2.visit
}
//SM is unique for a specific store, and its related ticket/visit queue
fact SMUniqueness{
no disjoint s1,s2: Store | s1.ticketqueue.manager=s2.ticketqueue.manager
and s1.visitqueue.manager=s2.visitqueue.manager
and s1.ticketqueue.manager=s2.visitqueue.manager
and s1.visitqueue.manager=s2.ticketqueue.manager
}
//different tickets/visits associated with the same user have different time
fact UniqueTimeUser {
all u: User, t1, t2: Ticket, v1,v2:Visit | ((u in t1.owner) and (u in t2.owner) and (u in v1.owner) and (u in v2.owner)
and (t1 != t2) and (v1 !=v2))
implies (t1.time != t2.time)
and (v1.time != v2.time)
}
//different ticket and visit associated with the same user have different time
fact UniqueTimeUser2 {
all u: User, t: Ticket, v:Visit | ((u in t.owner) and (u in v.owner) )
implies (v.time != t.time)
}
//Maximum number of visit with the same time for category
fact MaxTime{
all v:Visit, c: Category |(( c in v.category)) implies #v.time< c.simultaneous_seats
}
//Considering meaningfull integer value
fact PossibleValues{
all c: Category | c.simultaneous_seats>1 and c.simultaneous_seats<5
all s: Store | s.max_simultaneous >0 and s.max_simultaneous<50
all t: Ticket | t.time.hour>7 and t.time.hour<21 and ((t.time.minute=15) || (t.time.minute=30) || (t.time.minute=45)) and t.time.second=0
all v: Visit | v.time.hour>7 and v.time.hour<21 and ((v.time.minute=15) || (v.time.minute=30) || (v.time.minute=45)) and v.time.second=0 and v.duration.hour=0 and v.duration.minute>0 and v.duration.minute=<30 and v.duration.second=0
all tq: TicketQueue | tq.max_visit=32
}
pred addTicket[ t :Ticket,ti,ti':Time, tq, tq':TicketQueue]{
//precondition
ti' not in Ticket.time
#tq.ticket< tq.max_visit //seats available
//postconditions
tq'.manager= tq.manager
tq'.ticket= tq.ticket+t
t in tq'.ticket
#tq'.ticket< tq.max_visit
all t': Ticket | t' in tq.ticket implies t' in tq'.ticket
}
pred show{
#User = 4
#Store = 2
#SM = 2
#Category = 3
#TicketQueue = 2
#VisitQueue= 2
#Category = 5
some v, v': Visit | v.time != v'.time
#Ticket = 5
#Visit=5
}
run show for 4
This is the complete response of Alloy terminal: Executing "Run show for 4" Solver=sat4j Bitwidth=4 MaxSeq=4 SkolemDepth=1 Symmetry=20 15098 vars. 840 primary vars. 17697 clauses. 28ms. No instance found. Predicate may be inconsistent. 1ms.
