\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}