\documentclass[11pt]{article}
\usepackage{oz}
\def\Out#1{#1 \!\!\rightarrow}
\def\In#1{\rightarrow\!\! #1}
\begin{document}
Multi-letter identifiers have been changed to look
better than they do with vanilla \LaTeX: instead of
$\mathit{specifications}$, you get $specifications$.
The letters haven't been spread apart, and the
ligature $fi$ has been used.
{\tt This is in typewriter font}
\begin{schema}{BirthdayBook}
known: \pset NAME \\
birthday: NAME \pfun DATE
\ST
known = \dom birthday
\end{schema}
\begin{axdef}
limit : \nat
\ST
limit \leq 65536
\end{axdef}
\begin{class}{Shape}
\also
colour : Colour \\
\end{class}
\begin{axdef}
perim : \real
\ST
perim > 0
\end{axdef}
\begin{axdef}
ini:State \cross Occ \cross T \fun Bool
\where
\forall S:State, i: Occ, t:T \dot ini(S,i,t) \iff \\
\t1 \theta(\Out{S}, 1,0)\land\\
\t2 \exi t_{1}:T \dot \theta(\In{S},i,t_{1}) \land
t_{1}\leq t \land \forall t_{2}:T \dot t_{2} < t \imp \neg \theta(\Out{S},i+1,t_{2}
)\\
\t1 \lor \theta(\In{S}, 1,0)\land\\
\t2 \exi t_{1}:T \dot \theta(\In{S},i,t_{1}) \land
t_{1}\leq t \land \forall t_{2}:T \dot t_{2} < t \imp \neg
\theta(\Out{S},i,t_{2})
\end{axdef}
Let us see if \verb|zbreak| works:
\typeout{*************************************}
\typeout{If you get large overfull vboxes now, Oz is not working}
\typeout{*************************************}
\def \comm{\comment}
\begin{schema}{MakePlan}
c? : Company \comm{The company that is making the plan}\\
t? : Month \comm{Time period} \\
\Xi NFMM \\
\Xi AttrOfMarkets \comm{OpenMarkets} \\
\Xi Cost \\
\Xi AttrOfEconomy \comm{Buying and selling price of quota }\\
\Xi AttrOfQuota \\
\Xi AttrOfProduction \\
\Xi FishingLimitations \\
Plans! : Company \fun Plan \comm{The output is the plan for
the company} \\
\zbreak
\where
\forall v: Vessel; f: Fishery; s: QuotaStock; p: Product; \\
\t0 l: Landing; t: Month; i: Input @ \\
\t0 \exists plan: Plan; Months: \power Month; \\
\t0 vs : \power Vessel; fs: \power Fishery ; qs: \power QuotaStock; ls: \power Landing; \\
\t0 ps : \power Product; \\
\t0 catch: Vessel \cross Fishery \cross QuotaStock \pfun Tons; \\
\t0 MAXnet\_profit:Kronur; fishing\_cost:Kronur; \\
\t1 production\_earnings:Kronur; \\
\t1 production\_cost:Kronur; quota\_trading\_profit:Kronur; \\
\t0 fishing\_days: Vessel \cross Fishery \cross Month \pfun \nat; \\
\t0 value\_landing: Vessel \fun Kronur; \\
\t0 export: Vessel \cross Landing \cross Month \pfun Tons; \\
\t1 trade\_in, trade\_out: Landing \cross Month \pfun Tons; \\
\t1 prod: Product \cross Month \fun Tons; \\
\t0 quota\_rent\_in, quota\_rent\_out, quota\_next\_to, \\
\t1 quota\_next\_from, quota\_exch\_to, quota\_exch\_from,\\
\t1 quota\_trans\_from, quota\_trans\_to: Vessel \cross QuotaStock \pfun Tons; \\
\t0 ExchangeCharge: \num; \comm{charge for changing one species into another} \\
\t0 quota\_used: Vessel \cross QuotaStock \pfun Tons @ \\
\zbreak
\t0 Plans! = Plans! \oplus \{c? \mapsto plan \} \land \\
\t0 Months = t? \upto 12 \land \\
\t0 i \in Inputs \land \\
\t0 vs = Vessels ~ c? \land v \in vs \land\\
\t0 fs = \{f: Fishery | f \in \\
\t1 (\bigcup \{ v: Vessel | v \in vs @ Fisheries(v) \}) @ f \} \land f \in fs \land \\
\t0 qs = \{s: QuotaStock; f: Fishery | \\
\t1 f \in fs \land s \in QuotaStocks (f) @ s \} \land s \in qs \land \\
\t0 ls = \{s: QuotaStock; f: Fishery | f \in fs \land s \in qs @ \\
\t1 Landings~(f,s) \} \land l \in ls \land \\
\t0 ps = \{p: Product | \\
\t1 p \in \bigcup \{ fa: Factory | fa \in Factories~c? @ Products(fa) \} @ p \} \land \\
\t0 p \in ps \land \\
\comm{The overall goal is to maximize net profits} \\
\t0 MAXnet\_profit = -fishing\_cost+production\_earnings + \\
\t1 -production\_cost + quota\_trading\_profit \land \comm{A.1}\\
\t0 catch ~(v,f,s) = ExpCatch~(v,f,s)* \comm{A.4}\\
\t1 \sum_{t: Month | t \in Months} fishing\_days~(v,f,t) \land \\
\comm{One of the prices LandingPrice or ExportPrice is always zero for any l} \\
\t0 (\forall l | l \in ls @ LandingPrice (l) = 0 \lor ExportPrice(l) = 0 \land \\
\t1 LandingPrice(l) \neq ExportPrice(l) ) \land \\
\t0 value\_landing= \comm{A.3} \\
\t1 \{v: Vessel | v \in vs @ v \mapsto \\
\t1 \sum_{ l: Landing | l \in ls} LandingPrice (l)* ExportPriceConst(l) * \\
\t1 \sum_{f: Fishery | f \in fs} \sum_{s: QuotaStock | s \in qs} (SpeciesToLandings~(s,f,l) *(catch~(v,f,s)) \}\land \\
\t0 fishing\_cost = \sum_{v: Vessel | v \in vs} Share (v)*value\_landing(v) + \comm{A.2}\\
\t1 \sum_{ f: Fishery | f \in fs} CostFishDay ~ (v, f) * \\
\t1 \sum_{t: Month | t \in Months} fishing\_days~(v,f,t) \land \\
\zbreak
\t0 production\_earnings = \comm{A.5}\\
\t1 \sum_{l: Landing | l \in ls} \sum_{ t: Month | t \in Months} \\
\t3 (ExportPrice~(l,t))*(1-0.002)*t)* \\
\t3 \sum_{v: Vessel | v \in vs} export~(v,l,t) \\
\t1 -WetfishBuyingPrice(l) * (1-0.002)*t)*trade\_in~(l,t) \\
\t1 +WetfishSellingPrice(l) * (1-0.002)*t)*trade\_out~(l,t) \\
\t1 +\sum_{p: Product | p \in ps} ProductPrice~(p,t) *(1-0.002)*t)* \\
\t1 \sum_{t:Month | t \in Months} prod~ (p,t) \land \\
\t0 production\_cost = \sum_{i: Input | i \in Inputs} InputCost(i)* \comm{A.6}\\
\t1 \sum_{p: Product | p \in ps} InputForProduct(p,i) * \\
\t1 \sum_{ t: Month | t \in Months} prod(p,t) \land \\
\t0 ExchangeCharge = 0.005*NextPrice(s) \land \\
\t0 quota\_trading\_profit = -(\sum_{s: QuotaStock | s \in qs } QuotaRentInPrice(s) * \\
\t1 \sum_{v: Vessel | v \in vs } quota\_rent\_in~(v,s) ) \comm{A.7}\\
\t1 + \sum_{s: QuotaStock | s \in qs } QuotaRentOutPrice(s)* \\
\t1 \sum_{v: Vessel | v \in vs } quota\_rent\_out~(v,s) \\
\t1 + \sum_{s: QuotaStock | s \in qs } NextCharge *NextPrice(s)*(1-InterestRate)* \\
\t1 \sum_{v: Vessel | v \in vs } quota\_next\_to~(v,s) \\
\t1 + \sum_{s: QuotaStock | s \in qs } NextPrice(s)*(1-InterestRate) * \\
\t1 \sum_{v: Vessel | v \in vs } quota\_next\_from~(v,s) \\
\t1 -ExchangeCharge*\sum_{v: Vessel | v \in vs }\sum_{s: QuotaStock | s \in qs } quota\_exch\_to(v,s) \\
\t1 -TransferCharge*\sum_{v: Vessel | v \in vs }\sum_{s: QuotaStock | s \in qs } quota\_trans\_to~(v,s) \land \\
\t0 \sum_{ f: Fishery | f \in fs } fishing\_days~(v,f,t) \leq MaxTotFishingDays ~(v,t) \land \comm{A.9}\\
\comm{A.6.1 Constraints on fishing time } \\
\t0 l \in ExportLandings \implies \\
\t1 \sum_{f: Fishery | f \in fs } \sum_{s: QuotaStock | s \in qs } \comm{A.10} \\
\t2 SpeciesToLandings~(s,f,l) * ExpCatch (v,f,s)*fishing\_days(v,f,t) = \\
\t3 export~(v,l,t) \land \\
\comm{A.6.2 Processing and selling the catch } \\
\t0 l \notin ExportLandings \implies \\
\t1 \sum_{v: Vessel | v \in vs } \sum_{f: Fishery | f \in fs } \sum_{s: QuotaStock | s \in qs } \\
\t2 SpeciesToLandings~(s,f,l)*ExpCatch~(v,f,s)*fishing\_days~(v,f,t) \\
\t1 = (1 / LandingsToProducts~(p,l)) * prod~(p,t) - trade\_in~(l,t) + trade\_out(l,t) \land \comm{A.11}\\
\zbreak
\t0 \sum_{t: Month | t \in Months } \sum_{p:Product | p \in ps }InputForProduct(p,i)*prod(p,t) \\
\t1 \leq \sum_{i : Input | i \in Inputs } MaxInput~(i,t) \land \comm{A.13}\\
\t0 \sum_{t: Month | t \in Months } \sum_{p: Product | p \in ps } InputForProduct(p,i)*prod~(p,t) \\
\t1 \geq \sum_{i: Input | i \in Inputs } MinInput~(i,t) \land \comm{A.14}\\
\t0 \sum_{t: Month | t \in Months } export~(v,l,t) \leq MaxExport~(v,l) \land \comm{A.15}\\
\comm{A.6.3 Constraints because of quota restrictions } \\
\t0 quota\_used = \comm{A.17} \\
\t1 \{ v:Vessel; s: QuotaStock | v \in vs \land s \in qs @ \\
\t2 (v,s) \mapsto \sum_{f: Fishery | f \in fs } (1+QuotaSurcharge~(s,f))* \\
\t2 catch~(v,f,s) \} \land \\
\t0 \sum_{v: Vessel | v \in vs } quota\_trans\_to(v,s)- quota\_trans\_from(v,s) =0 \land \comm{A.18} \\
\t0 quota\_used(v,s) - quota\_rent\_in(v,s) + quota\_rent\_out(v,s) - \comm{A.16} \\
\t1 quota\_exch\_to(v,s) + quota\_exch\_from(v,s) - \\
\t1 quota\_trans\_to(v,s) + quota\_trans\_from(v,s) - \\
\t1 quota\_next\_to~(v,s) + quota\_next\_from~(v,s) \leq QuotaLeft~(v,s) \land \\
\t0 s = Cod \implies MaxQuotaInto(v,s) = 0 \land \comm{A.19}\\
\t0 s \neq Cod \implies MaxQuotaInto(v,s) = 0.05*QuotaAllocated(v,s) \land \\
\t1 QuotaValueInto(s)*quota\_exch\_to(v,s) \leq \\
\t2 \sum_{s: QuotaStock | s \in qs } MaxQuotaInto~(v,s) \land \\
\t0 \sum_{s: QuotaStock | s \in qs } QuotaValueInto (s)*quota\_exch\_to~(v,s) - \comm{A.20}\\
\t1 \sum_{s: QuotaStock | s \in qs } QuotaValueFrom(s)* quota\_exch\_from~(v,s) = 0 \land \\
\t0 quota\_next\_from(v,s) \leq (QuotaOver(v,s) / 100)*QuotaAllocated(v,s) \land \comm{A.21}\\
\t0 quota\_next\_to~(v,s) \leq (QuotaUnder(v,s) / 100)*QuotaAllocated(v,s) \land \comm{A.22} \\
\zbreak
\comm{Bounds} \\
\t0 fishing\_days~(v,f,t) \leq MaxFishingDays~(f,t) \land \comm{A.23}\\
\t0 QuotaAllocated~(v,s) = 0 \implies \\
\t1 (quota\_exch\_to~(v,s) = 0 \land \comm{A.24}\\
\t1 quota\_rent\_in~(v,s) = 0 \land \comm{A.25}\\
\t1 quota\_trans\_to~(v,s) = 0) \land \comm{A.26} \\
\t0 QuotaValueInto~s = 0 \implies quota\_exch\_to~(v,s) = 0 \land \comm{A.27}\\
\t0 QuotaValueFrom~s = 0 \implies quota\_exch\_from~(v,s) = 0 \comm{A.28}\\
\zbreak
\t0 plan.c = c? \
\t0 plan.fishing\_days = fishing\_days \land
\t0 plan.quota\_rent\_out = quota\_rent\_out \land \\
\t0 plan.quota\_rent\_in = quota\_rent\_in \land \\
\t0 plan.quota\_trans\_from = quota\_trans\_from \land \\
\t0 plan.quota\_trans\_to = quota\_trans\_to \land \\
\t0 plan.quota\_next\_from = quota\_next\_from \land \\
\t0 plan.quota\_next\_to = quota\_next\_to \land \\
\t0 plan.quota\_exch\_from = quota\_exch\_from \land \\
\t0 plan.quota\_exch\_to = quota\_exch\_to \land \\
\t0 plan.trade\_out = trade\_out \land \\
\t0 plan.trade\_in = trade\_in \land \\
\t0 plan.prod = prod \land \\
\t0 plan.export = export \\
\end{schema}
\end{document}