In order to be able to have a more sensible understanding of ASML, but also to learn how to use ASML modeling, we may wish to study an instance of an ASML. The following example is a Word version of a design specification written with ASML, which comes from an example of ASML2.1.5.8 - Diningphilosophers. For ease of understanding, I translated it into Chinese. More ASML examples can be found in the Sample Folder of ASML.
Dijkstra's philosopher FSE COPYRIGHT (C) Microsoft Corporation. All Rights Reserved. 1 Embedding This example is part of the name space below:
Namespace Diningphilosophersophersophers
A group of philosophers sitting at the table. There is a meal fork on the left and right side of each person. We use this below only one domain index structure to define the meal fork:
Structure fork
Index as in
Philosophers are defined as a unique index that reflects the status of their current situation, as well as the following two capabilities: reporting whether they can change the status (canmove), and changeable changes (MOVE). Because Status can change, philosophers are Class instead of structure.
Abstract Class Philosopher
Var status as state = thinking
Index as in
Abstract Canmove (Table as Table) as boolean
Abstract Move (Table as Table)
For the sake of simplicity, we assume that the philosophographer has a fixed number (5).
Numphilosophers as integer = 5
Similarly, we have five meals forks.
NumForks as integer = NUMPHILOPHERS
Forks as set of fork = {fork (i) | i in {1..numForks}}
The philosophers have the same index on the left side of the philosopher. The index of the stemers on the right side of the philosopher is larger (the model of the total number of philosophers).
Left (P as philosopher) as fork
Return fork (p.index)
Right (p as philosopher) as fork
Return Fork (P.index Mod Numphilosophers 1)
Thinking about the philosopher no food fork. (Who needs a meal fork to think?) Thinking about the philosopher in the middle of the philosophers may become hungry. Hungry philosophers tried to get the meal fork on the left to become "hungry philosophers who took the food fork." But only a meal fork is not enough, only two meals fork philosophers began to eat. Only the on-right meal can only be obtained when no one is used. After eating things, the philosopher only one thing can be done, that is, putting down two meal forks to continue thinking. So, a successful philosopher is eating something: thinking -> Hungry -> Hungrywithleftfork -> Eating -> thinking
ENUM
State
Thinking
Hungry
Hungrywithleftfork
Eating
We now define a table for these five philosophers:
Class Table
Philosophers as set of philosopher
Use a variable to describe which philosophers are using it. Another variable defines a collection of philosophers who are eating:
Class Table
Var Holder as map of fork to philosopher = {->} var fed as set of philosopher = {}
The following method describes the action of philosophers. Active philosopher can be randomly selected. If there is no philosopher to move, then a deadlock has happened.
Class Table
Var Stepno As INTEGER = 0
[Entrypoint]
Move ()
Choose Phil in Philosophers Where Phil.canmove (ME)
Phil.Move (ME)
Stepno: = STEPNO 1
EntryPoint enables marked methods to be called by external world, for example, can be called by C #. 2.1 Greedy Philosophersophers' greedy philosophers will never let go of the meal fork before you have finished eating things and start thinking, which will cause a deadlock.
Class Greedyphilosopher Extends Philosopher
Override Move (Table as Table)
Match status
Thinking: status: = hungry
Hungry: if not (Left (me) in table.holder
Table.Holder (Left (me): =
ME as philosopher
Status: = hungrywithleftfork
Hungrywithleftfork
: IF not (Right (ME) in Table.Holder
Table.holder (Right (me): =
ME as philosopher
Status: = eating
Add me to Table.FED
Eating: Remove Table.holder (Left (me))
Remove Table.Holder (Right (ME))
Status: = thinking
Canmove method points to whether a philosopher can change:
Class Greedyphilosopher
Override Canmove (Table as Table) AS Boolean
Return status = thinking
OR (status = hungry and
Left (me) notin table.holder)
or (status = hungrywithleftfork and
Right (me) notin table.holder)
OR status = Eating
2.2 Generous Philosophers' generous philosophers do not stick to life of a successful philosophers. After getting the fork of the left hand, if you find that you can't get the right hand, generous philosophers will put down the left hand meals fork and continue to think about it. Therefore, if everyone is a generous philosopher, then there will be no dead lock, but some people may starve. :)
Class generousphilosopher extends philosopher
Override Move (Table as Table)
Match status
Thinking: status: = hungry
Hungry: if not (Left (me) in table.holder
Table.Holder (Left (me): =
ME as philosopher
Status: = hungrywithleftfork
Hungrywithleftfork
: IF not (Right (ME) in Table.Holder
Table.hold (Right (ME): = me as philosopher
Status: = eating
Add me to Table.FED
Else
// Someone else is Holding the
// Right Fork
// Put the Left One Down and
// Try Again ANOTHER TIME
Remove Table.holder (Left (me))
Status: = thinking
Eating: Remove Table.holder (Left (me))
Remove Table.Holder (Right (ME))
Status: = thinking
Note that the conditions that determine whether the generous philosophers can change to the greedy philosophers.
Class menerousphilosopher
Override Canmove (Table as Table) AS Boolean
Return status = thinking
OR (status = hungry and
Left (me) notin table.holder)
OR status = hungrywithleftfork
OR status = Eating
3 Providing The View We offer two ways to initialize, an initialized greedy philosophers, another initialized generous philosophers.
Class Table
[Entrypoint]
Shared initgreedy () as table
Philosophers = {New Greedyphilosopher (i) as philosopher |
I in [1..numphilosophers]}
Return New Table (Philosophers)
[Entrypoint]
Shared initGenerous () as table
Philosophers = {new generousphilosopher (i) as philosopher |
I in [1..numphilosophers]}
Return New Table (Philosophers)
Give the index of philosophers, the following methods will point out that the philosopher has a meal fork, and whether it is eating.
Class Table
HoldsLeft (Pindex as integer) as boolean
Return EXISTS (I, P) in Holder Where P.index = PINDEX AND
LEFT (P) = i
Holdsright (PINDEX As INTEGER) AS Boolean
Return EXISTS (I, P) in Holder Where P.index = PINDEX AND
Right (p) = i
Isfeeded (pindex as integer) AS Boolean
Return EXISTS P IN FED Where P.index = PINDEX
IsdeAdlock () as boolean
Return Forall P in Philosophers Holds Not P.canmove (ME)
Isgreedy () as boolean
Return EXISTS P IN Philosophers Where P Is Greedyphilosopher
Stepno () AS Integer
Return Stepno
This article is intended to introduce
ASML
. Since the author has just been in contact
ASML
