Demo entry 6322483

prova

   

Submitted by anonymous on Nov 12, 2016 at 10:22
Language: Alloy. Code size: 6.6 kB.

------------------------------------Position things--------------------

sig Position{
	latitude: Int,
	longitude: Int
}{
	latitude >=0
	latitude <=3
	longitude >=0
	longitude <=5
}

//the positions are uniquely determinate by the place
fact differentPosition{
	all p1, p2: Position| (p1!=p2)implies(p1.latitude != p2.latitude or p1.longitude != p2.longitude)
}

------------------------------------Safe Areathings--------------------

sig SafeArea{
	safePositions: some Position,
}

fact differentPositionInDifferentSafeArea{
	all s1,s2: SafeArea| all p: s1.safePositions| (s1 !=s2) implies ((p in s1.safePositions) and (p not in s2.safePositions))
}

//in our world there are always unsafe position
fact positionConstraint{
	all s: SafeArea| some p: Position| p not in s.safePositions
}

---------------------------------Special Area things--------------------

sig SpecialArea{
	specialPositions: some Position,
	plugs: Int,
}{
	plugs >=0
	plugs <=5
}

fact plugsConstarint{
	all s:SpecialArea| #(s.specialPositions) = s.plugs
}

fact specialAreaConstraint{
	all p: SpecialArea.specialPositions | (p in SafeArea.safePositions) &&
	(#(SpecialArea.specialPositions) < #(SafeArea.safePositions))
}

fact differentPositionInDifferentSecialArea{
	all s1,s2: SpecialArea| all p: s1.specialPositions| (s1 !=s2) implies ((p in s1.specialPositions) and (p not in s2.specialPositions))
}

----------------------------------------Car things--------------------

//there are no less than two seats 
sig Car{
	code: Int,
	seats: Int,
	state: one State,
}{
	code>=0
	seats>=2
	seats<=5
}

fact indentificationByCode{
	all c1, c2: Car | (c1 != c2) implies (c1.code != c2.code)
}

pred Car.isUsed[]{
	#(this.state.usedBy)=1
}

pred Car.isInSafe[]{
	one s: SafeArea| this.state.statePosition in s.safePositions
}

pred Car.isInSpecial[]{
	one s: SpecialArea| this.state.statePosition in s.specialPositions
}

pred Car.isAvailable[]{
	!(this.isUsed) and (this.state.batteryLevel >1) and (this.isInSafe)
}

pred Car.isNotAvailable[]{
	this.isUsed or this.state.batteryLevel <1 or !(this.isInSafe)
}

pred Car.isInList[l1:List]{
	this in l1.cars
}
----------------------------------------State things--------------------

sig State{
	batteryLevel: Int,
	phase: one Phase,
	passengers: Int,
	statePosition: one Position,
	usedBy: lone User
}{
	//per future implementazioni meglio passenges > < seats dell'auto
	passengers >=0
	batteryLevel >=0
	batteryLevel <=3
}

fact numberOfState{
	#Car = #State
}

fact passengersConstraint{
	all c:Car| ((c.state.phase=used) implies (c.state.passengers<=c.seats)) and((c.state.phase!=used) implies (c.state.passengers=0))
}

//this means that there are not cars in the same position
fact differentPositionInCar{
	all c1,c2 : Car | (c1!=c2) implies (c1.state.statePosition != c2.state.statePosition)
}


----------------------------------------Phase things--------------------

//these are the possible internal state of the car
enum Phase {reserved, used, charge, free, parkUnsafeOrCharge}

fact reservedPhase{
	all c: Car| (c.state.phase = reserved) iff (c.isInSafe and c.state.batteryLevel>1 and c.isUsed and (c.state.phase!=used and c.state.phase!=charge and c.state.phase!=free and c.state.phase!=parkUnsafeOrCharge))//	batteryLevel >=1 usata
}

fact usedPhase{
	all c: Car| (c.state.phase = used) iff (c.isUsed and c.state.batteryLevel != 0  and (c.state.phase!=reserved and c.state.phase!=charge and c.state.phase!=free and c.state.phase!=parkUnsafeOrCharge)) //batteria >0 e deve essere usata
}

fact chargePhase{
	all c: Car| (c.state.phase = charge) iff (!(c.isAvailable) and c.isInSpecial and (c.state.phase!=reserved and c.state.phase!=used and c.state.phase!=free and c.state.phase!=parkUnsafeOrCharge))//	position in special e non è usata
}

fact freePhase{
	all c: Car| (c.state.phase = free) iff (c.isAvailable and (c.state.phase!=reserved and c.state.phase!=used and c.state.phase!=charge and c.state.phase!=parkUnsafeOrCharge))//	batteria maggiore di 1 non è usata non è in carica
}

fact parkUnsafePhase{
	all c: Car| (c.state.phase = parkUnsafeOrCharge) iff (!(c.isAvailable)and /*(c.isInSafe or !(c.isInSafe)) and */ (c.state.phase!=reserved and c.state.phase!=used and c.state.phase!=charge and c.state.phase!=free))//	posizione è in unsafe e non è usata
}


----------------------------------------User things--------------------

sig User {
	licenseID: Int, //should be an alphanumeric value in the real world
}{
	licenseID > 0
}

//this means that there are not equal users
fact differentIDUser{
	all u1, u2: User | (u1 != u2) implies (u1.licenseID != u2.licenseID)
}

fact differentUserOnCar{
	all c1,c2: Car| (c1 != c2) implies (c1.state.usedBy != c2.state.usedBy)
}

----------------------------------------Employee things--------------------

sig Employee {
	employeeID: Int,
} {
	employeeID > 0
}

fact uniqueEmployee{
	all e1,e2: Employee| (e1 != e2) implies (e1.employeeID != e2. employeeID)
}

----------------------------------------PairOfWorkers things--------------------

sig PairOfWorkers {
	employees: some Employee
} {
	#employees = 2
}

fact uniquePairOfWorkersForEmployee {
	all e :Employee| lone p : PairOfWorkers| ((e in p.employees)) 
}

fact mapPairOfWorkersOnLists{
	#PairOfWorkers = #List
}

fact differentPairPerList{
	all l1,l2: List| (l1!=l2) implies (l1.pair!=l2.pair)
}

----------------------------------------List things--------------------

sig List{
	code: Int,
	cars: some Car,
	pair: one PairOfWorkers,
}{
	code>0
	#cars>0
}

fact uniqueList{
	all l1,l2: List| (l1!=l2) implies (l1.code!=l2.code)
}



fact phaseOfCarInTheList{
	all c: List.cars| c.state.phase=parkUnsafeOrCharge
}

fact phaseOfCarInTheList{
//	all c:Car| one l:List| (c.state.phase=parkUnsafeOrCharge) implies (c in l.cars)
}


fact differentList{
	all l1,l2: List| all c: l1.cars| (l1!=l2) implies !(c.isInList[l2])
}

fact listConstraints{
	all c:Car| (c.state.phase=parkUnsafeOrCharge) implies (c in List.cars)
}


pred show(){
//some c:Car| c.state.phase=reserved
//some c:Car| c.state.phase=used
//some c:Car| c.state.phase=charge
//some c:Car| c.state.phase=free
//some c:Car| c.state.phase=parkUnsafeOrCharge
// l: List| #(l.cars) =2
}

run show for 1  but  exactly 15 Position, exactly 1 SafeArea, exactly 2 SpecialArea, exactly 7 Car, exactly 7 State, exactly 6 User, exactly 5 Employee, exactly 2 PairOfWorkers, exactly 2 List

This snippet took 0.01 seconds to highlight.

Back to the Entry List or Home.

Delete this entry (admin only).