-- MEI case study (14/15)

-- version of Thu 8 Nov

open RelCalc

--- Data model 

sig D, H {}

sig A {
    R : set P,
    S : set U
}

sig P {
   d : one D
}

sig U {
    p: one P,
    h : one H
}

--- Invariant properties
 
-- I1: perfis de um mesmo aluno em dias diferentes
pred inv1 { img[R] & ker[d] in iden }

-- I2: complementares de um mesmo aluno em dias/horas diferentes
pred inv2 { img[S] & ker[h] & ker[p.d] in iden }

-- I3: UCs complementares e UCs de perfil em dias diferentes
pred inv3 { no (R . d.~d.~p.~S & iden)  } 

-- I4: os perfis ocupam dias inteiros
pred inv4 { (P->H) in ~p.h } 

run {
    inv1
    inv2
    inv3
    inv4
    not ((P->P) in ker[d]) -- rule out the annoying constant function! 
}