open util/integer

--UNIX time notation
--Dates are the number of seconds from a reference date (for example 1th January 2018)

--SIGNATURES--
sig Float{}

abstract sig Bool{}
one sig True extends Bool{}
one sig False extends Bool{}

--it's the position of the user or the location searched by a company query
sig Location{
--latitude
lat: one Float,
--longitude
long: one Float}

--the possible criteria that a company can choose
-- for selecting a precise group of people in a query
sig Criteria{
--age criteria
age: lone Int,
--location criteria
loc: lone Location,
--gender criteria: female = 0, male = 1
gen: lone Bool}
{age>0}

--the possibile answer given
sig Answer{
--response
answer: lone Bool,
--id query that refers to the query
idQuery: one Int}
{idQuery>0}

--There are all the possible status of query is
 abstract sig StatusQuery{}
one sig SENT extends StatusQuery{}
one sig ACCEPTED extends StatusQuery{}
one sig DENIED extends StatusQuery{}

--The structure of a query from a company
sig Query{
--unique for each query
idQ: one Int,
--answer/s of the query
ans: set Answer,
--criteria of the query
crit: one Criteria,
--company that asks this query
comp: one Company,
--status of the query
status: one StatusQuery}
{idQ>0 and
status = ACCEPTED implies (one a: ans | a.idQuery = idQ and a.answer = True)
status = DENIED implies (one a: ans | a.idQuery = idQ and a.answer = False) and
--all set of answer in query structure has to be related to that query
all a: ans | a.idQuery = idQ
}


--parameters of health
sig Cardiac{
--first parameter : cardiac Rate
p1: lone Float,
--date ( year month day hour minute second ) of each parameter
date: one Int}
{date>0}

--The health status of each user
sig Health{
--fiscal code of the user
fC: one String,
--the cardiac rate of the user
cardiac: one Cardiac,
-- the position od the user
position: one Location,
--1 if is older than 60, 0 otherwise
over60: one Bool,
--1 if the ambulance is sent for an emergency
ambulanceSent: one Bool}

--the warn that health parameter are under a certain threshold
sig Warn{}

--abstract structure for all users subscribed
abstract sig UserSubscribed{
--name of the company or the user
name: one String,
--password of the selected by the user
password: one String,
-- email used to register the user
email: one String
}

--individual that download the app and register himself
one sig User extends UserSubscribed{
--id that identify in a unique way each user
fiscalCode: one String,
--gender of the user
gender: one Bool,
--date of the birth day
birthDay: one Int,
--age of the user
age: one Int,
--all the answers given by the user
answeredQueries: set Answer,
--all the warn given by the system
warns: set Warn,
--the heathStatus of the user
healthS: one Health}
{age>0}

--the third company that asks queries to the system
one sig Company extends UserSubscribed{
--id that identify in a unique way each company
vta: one Int,
--all the queries asked by the company
askedQueries: set Query,
--receivedHealthStatus
receivedHealthStatus: set Health
}
{vta>0}


--FACTS--
-- No two distinct coinciding users
fact OnlyUniqueUserSubscribed{
no disj u1, u2: UserSubscribed | u1!=u2 and u1.email = u2.email}

--No two distinct users with the same fiscal code
fact OnlyUniqueUser{
no disj u1, u2: User | u1!=u2 and u1.fiscalCode = u2.fiscalCode}


--No two distinct companies with the same vta
fact OnlyUniqueCompany{
no disj c1, c2: Company | c1!=c2 and c1.vta = c2.vta}


--No two distinct queries with the same id
fact OnlyUniqueQueries{
no disj q1,q2: Query | q1!=q2 and q1.idQ = q2.idQ}

--ASSERTIONS--
--all answers has to be linked to a query
assert AnswersRelatedToQuery{
all a: Answer | one q: Query | q in a.idQuery
}


--PREDICATES--
pred sympleShow{
#User <=2
#Company <=1
some q : Query | q.status = ACCEPTED
some a : Answer | a.answer= True
}

pred complexShow{
#User >1
#Company >1
some q : Query | q.status = ACCEPTED
some a : Answer | a.answer= True
}

--run sympleShow for 6 but 8 int
run sympleShow for 2 but exactly 10 String