
\MODEL{CoursePlan}
\SORTS

$\begin{array}{lcll}
Plan & \cong & {\set{Course}} & 
\INV{p} = 
\LET 
coll = 
\LAMBDA{x}.
\CASE 
\is{Mandatory}(x) \VALUE 
Ym(x) \\ 
\is{Optional}(x) \VALUE 
Yo(x) 
 \ESAC
  
\IN 
\exists x \in \{6,5,4,3,2,1\} : 

coll(p) = 
inseg(x) 
\TEL \\
Course & \cong & {Mandatory + Optional} &  \\
Mandatory & \cong & 
\PROD Ym \TYPE Year \NEXT Am \TYPE Area \NEXT Nm \TYPE Name \DORP
 &  \\
Optional & \cong & 
\PROD Yo \TYPE Year \NEXT Io \TYPE Idf \NEXT Ops \TYPE {\set{Option}} \DORP
 &  \\
Option & \cong & 
\PROD Ao \TYPE Area \NEXT No \TYPE Name \DORP
 &  \\
Year & \cong & INT &  \\
Area & \cong & STR &  \\
Name & \cong & STR &  \\
Idf & \cong & INT &  \\
\end{array}$

\OPERS

\STATE{P}{Plan}
$\begin{array}{l}
invariant() \deff \\ \rule{3ex}{0pt} 
inv\_Plan(P)
\end{array}$

\traco

$\begin{array}{l}
x: \tfunc{} \\ x() \deff \\ \rule{3ex}{0pt}  
\COND{
x = true}{true}{false}
\end{array}$

\traco

$\begin{array}{l}
InsMC:Year \times Area \times Name \tfunc{} \\ InsMC(y,a,n) \deff \\ \rule{3ex}{0pt}  P' = P \cup \{
Mandatory(y,a,n)\}
\end{array}$

\traco

$\begin{array}{l}
InsOC:Year \times Idf \times {\set{Option}} \tfunc{} \\ InsOC(y,i,o) \deff \\ \rule{3ex}{0pt}  P' = P \cup \{
Optional(y,i,o)\}
\end{array}$

\traco

$\begin{array}{l}
Courses: \tfunc{{\set{Name}}} \\ Courses() \deff \\ \rule{3ex}{0pt}  
\LET 
m = \{c \asor c \in P \wedge \is{Mandatory}(c)\}\\
o = P - m 
\IN 
Nm(m) \cup 
\bigcup (\{
No(
Ops(c)) \asor c \in o\}) 
\TEL
\end{array}$

\traco

$\begin{array}{l}
OptionalAreas: \tfunc{{\set{Area}}} \\ OptionalAreas() \deff \\ \rule{3ex}{0pt}  
\LET 
m = \{c \asor c \in P \wedge \is{Mandatory}(c)\}\\
o = P - m 
\IN 
\bigcup (\{
Ao(
Ops(c)) \asor c \in o\}) - 
Am(m) 
\TEL
\end{array}$

\traco
