# Modeling from A to Z/Modeling the Waste Management System
## Next Generation Nuclear Power Stations and Waste Management

It would appear that the Nuclear Power Station will be with us for the foreseeable future. Moreover, it is not so much the generation of electricity that matters but the management of the waste that results.
Waste management is not unique to the domain of nuclear power. The current need for a green revolution to undercut climate change and global warming depends crucially on how oil-related products such as plastics are re-cycled or incinerated. Illegal dumping is rife in many countries.
In this section we look at one aspect of waste management, adopted from the nuclear industry and show how it may be re-used for general waste management. In itself the development illustrate a general principle in (software) process improvement. Real systems evolve and migrate. They are very rarely begun from scratch. Any software development plan ought to follow the same process improvement of the system to match.
Tracking is just like searching. It relies on addresses. And now know that addressing may be a matter of placing cookies or RFID tagging.

### Sources of inspiration

We will begin our model by looking at some work already published. That is to say, we will not pretend any originality or creativeness. Our starting point will be a “tracking manager study” (TMS) which was carried out as part of the «Research Study into the use of Computer-based Tracking Systems as valuable support to Safety Cases in Nuclear Power Technology»
In essence there are two kinds of things: containers and what goes into them. The different kinds of containers are easy to point out. In the TMS there are 5 of them:
* crate
* package
* liner
* puck
* drum container
We already know from our earlier work on Alloy that we can introduce an abstract signature for Container and introduce the 5 container types as extensions:
   abstract sig Container sig Crate, Package, Liner, Puck, Drum extends Container
Those things that go into certain kinds of containers may be called materials. In our first study of the TMS we will look at just 4 material types:
* glass
* plastic
* metal
* liquor
Just as for Container above, so we introduce an abstract signature for Material and the four types of material then become extensions:
   abstract sig Material sig Glass, Plastic, Metal, Liquor extends Material
Finally, for this introduction, one notes that the phases of processing within the Waste Management System can be classified analogously:
   abstract sig Phase sig Unpacking, Sorting, Assaying, Compacting, Exporting extends Phase
Instead of using the term "Phase", one might prefer "Process". Here is the list of Phases modelled:
* Unpacking (crates)
* Sorting (contents)
* Assaying (materials)
* Compacting (materials)
* Exporting (stuff)

## Alloy model of the Tracking Management System (TMS)

This is a re-modelling of the tracker system described in
* John Fitzgerald and Cliff Jones, 1998, pp.1-28
* John. S. Fitzgerald, 1999, pp.69-94
* John Fitzgerald and Peter Gorm Larsen, pp. 137-201?

### Introductory text

A detailed formal model of a system is but one step away from implementation. That step consists of the working out of the formal mathematical expressions. Such working out is a mixture of hardware and software. Much of it will be off-the-shelf. Some of it will necessarily be hand crafted. But before we get to this stage of detail, we need an abstract bird's-eye view. This overview will capture everything in essence and will be comprehensible. Here is such an executive overview supported by Alloy.

### System requirements

A Tracking Management System (TMS) monitors the position of containers of material as they pass through the various phases of processing in an industrial plant (IP) such as a waste management facility (WMF).
Each container holds only one type of material and can be in at most one processing phase at a time.
Each processing phase has a maximum container capacity and can only accept certain types of materials.

### System state

At any point in time a system state of the TMS must record:
* The catalog of material type contents of each container in the WMS. Briefly, this is the simply denoted by the cntCatalog
* The collection of containers in each processing phase.
* The phase properties of each processing phase:
** the maximum container capacity (maxCapacity) and
** the acceptable types of materials (mtrType).

### System state constraints

At any point in time a system state of the TMS must satisfy the following system state constraints:
* Each container can hold at most one type of material. Each container can be in at most one processing phase at a given time. Each processing phase can have at most one value for it's maximum capacity.
* All processing phases have recorded phase properties: a maximum capacity and acceptable material types.
* Each processing phase in the industrial plant has a maximum capacity of at least one.
* The containers in any given processing phase all have recorded material contents.
* The active processing phases have recorded phase properties: a maximum capacity and acceptable material types.
* Each type of material in the IP has a possible processing phase.
* Each phase in the IP is operating within capacity.
* In any phase, all the containers in that phase have the expected kinds of materials inside them.

### System operations

The TMS has a number of operations which modify the system state:
* initOp: specifies the properties of an initial state of the TMS.
* insertOp: adds a new container whose contents are of a given material type to the industrial plant container catalogue. (was introduce operation)
* remOp: removes a container from given phase of processing
* delOp: deletes a container from both the container content catalogue and the tracker system.
* permitOp: which decides whether a container may be moved into a given phase.
* moveOp: moves a container into a given phase processing within the tracker system.

## Alloy module

   module TrackingManagementSystem -- abbreviated TMS
   open util/relation as rel -- Binary relation module. open util/natural as nat -- Natural number module. open util/boolean as bool -- Boolean module
   sig Container, Material, Phase -- Containers, material types, and processing phases.
   sig SystemState {
   cntCatalog: Container -> Material, -- The container catalogue.
   trkSystem: Container -> Phase, -- The tracker system.
   maxCapacity: Phase -> Natural, -- Phase max capacity record.
   mtrType: Phase -> Material -- Phase material types record.

## Visualization

We know from earlier work on Alloy that this is sufficient information for us to visualise the structure of the metamodel:

### System constraints

[1]
   pred FieldTypeCns(s: SystemState) {  functional[sysState.cntCatalog, dom[sysState.cntCatalog]]
    functional[sysState.trkSystem, dom[sysState.trkSystem]]  functional[sysState.maxCapacity, dom[sysState.maxCapacity]]  dom[sysState.maxCapacity] = dom[sysState.mtrType]  all phase: dom[sysState.maxCapacity] | sysState.maxCapacity[phase] != Zero }
[2]
   pred TrackerContainerCns(sysState: SystemState) {  dom[sysState.trkSystem] in dom[sysState.cntCatalog]
[3]
   pred TrackerPhaseCns(sysState: SystemState) {  ran[sysState.trkSystem] in dom[sysState.maxCapacity]  ran[sysState.trkSystem] in dom[sysState.mtrType] }

# A simpler waste management model
## Containers

Let us begin with the container? Imagine that you are in a building where there are containers for
* the disposal of empty water bottles,
* used ink-jet cartridges,
* used batteries, and
* waste paper.
These containers are collected by the garbage firm NoWasteNoWant once a week and brought to the waste-management facility in the city.

### Container notes

When we talk about "empty water bottles" we are thinking of either plastic or glass materials. For now, we will limit ourselves to just two types:
* glass bottle
* plastic bottle

## Container Types

For the sake of the first model on waste management. We will assume there are just two types of container:
* wet container — used for all liquid stuff, that is the plastic or glass bottles.
* dry container — used for everything else

# Notes

* ↑ TMS is our acronym. It stands for Tracking Manager Study. The use of acronyms in Computer Science is widespread. The habit is probably due to the very concept of programming variable. It would be nice to verify this hypothesis. We will use this acronym in our own model for the Waste Management System. But in this case, TMS will stand for Tracking Management System. Acronyms can be flexible, even if ambiguous.
* ↑ Fitzgerald&Jones 1998, p.28.
* ↑ Fitzgerald&Jones 1998, p.3
* ↑ The example of the Universal Puck at SLAC Stanford might give some idea of what sort of thing a puck is, what it might look like, and how it might be used.
* ↑ Report WSRC-MS-98-00571 gives a very good overview of nuclear waste management issues, including a very useful text on the use of the puck.
* ↑ Fitzgerald&Jones 1998, p.3.

# Reading links

* Bicarregui, Juan Carlos (editor), (1988). Proof in VDM: case studies. London: Springer-Verlag. ISBN 978-3540761860. {{cite book}}: |first= has generic name (help); Cite has empty unknown parameter: |coauthors= (help)CS1 maint: extra punctuation (link)
* Fitzgerald, John (1998). "A Tracking System". In Bicarregui, Juan Carlos (ed.). Proof in VDM: Case Studies. London: London: Springer-Verlag. pp. 1–29. {{cite book}}: Cite has empty unknown parameter: |coeditors= (help); Unknown parameter |coauthors= ignored (|author= suggested) (help)

# e-Links

* Nuclear power in France last access {2008-08-14}
* Universal Puck last access {2008-08-14}
* Report WSRC-MS-98-00571 Proposed New DOE Remote Facilities Overview - Designing for the Next Century last access {2008-08-15}
* World Intellectual Property Organization (WIPO): (WO/2006/005905) METHOD FOR THE HANDLING AND MINIMISATION OF WASTE last access {2008-08-14}