\begin{ffcode}
   sig Date {
	unixTime: one Int
    } {
    	unixTime >= 0
    }
    //Radomly chosen by Alloy
    one sig Now extends Date {}
    
    sig Location {}
    sig Email {}
    sig UserName {}
    sig Password {}
    sig CompanyName {}
    sig PaymentMethod {}
    
    abstract sig Bool {}
    one sig True extends Bool {}
    one sig False extends Bool {}
    
    sig User {
    	userName: one UserName,
    	email: one Email,
    	password: one Password,
    	paymentMethod: one PaymentMethod,
    	bookings: set Booking
    } {
    	//No user can have two overlapping bookings
    	all b1, b2: Booking | (b1 in bookings and b2 in bookings)
    	implies
    	(b1 = b2 or (b1.startDate.unixTime < b2.startDate.unixTime and b1.endDate.unixTime <= b2.startDate.unixTime) or
    	(b2.startDate.unixTime < b1.startDate.unixTime and b2.endDate.unixTime <= b1.startDate.unixTime))
    }
    
    //Force that a booking of a eMSP is made by a user registered in that eMSP, even tho the eMSP is only one...
    sig Booking {
    	startDate: one Date,
    	endDate: one Date,
    	isActive: one Bool,
    	socket: one Socket
    } {
    	startDate.unixTime < endDate.unixTime
    	and (isActive = True implies startDate.unixTime <= Now.unixTime and Now.unixTime <= endDate.unixTime)
    	and (isActive = True implies socket.connectedVehicle != none)
    }
    
    fact noBookingsWithoutUsers {
    	all b: Booking | (one u: User | b in u.bookings)
    }
    
    fact noExpiredBookings {
    	all b: Booking | b.endDate.unixTime >= Now.unixTime
    }
    
    fact noOverlappingSocketBookings {
    	/*
    	or ((b1.startDate.unixTime < b2.startDate.unixTime implies b1.endDate.unixTime <= b2.startDate.unixTime) and (b1.startDate.unixTime > b2.startDate.unixTime implies b2.endDate.unixTime <= b1.startDate.unixTime))
    	*/
    	all b1, b2: Booking | (b1 = b2 or b1.socket != b2.socket or (b1.startDate.unixTime < b2.startDate.unixTime and b1.endDate.unixTime <= b2.startDate.unixTime)
    	or (b2.startDate.unixTime < b1.startDate.unixTime and b2.endDate.unixTime <= b1.startDate.unixTime))
    }
    
    run {} for 12 but 6 Int, exactly 3 User, exactly 3 CS, exactly 2 CPMS, exactly 3 Booking
\end{ffcode}