Home

User Manual

Contents

1. utils the maximum of x utils z ze x and forall y x z lt y minimum of set x utils x min y utils min rng x is a registered trade mark of ASPT 76 Deloitte amp Touche Bakkenist AN min x num num minus x num num mod x num y num num mod x num y num num mod x num y num num mult x num y num num mult x num y num num mult n num x real real mult x real n num real mult x num n num num num x real num num x real y num num numlx str num numerator x num num odd n num bool pos x num bool pow x num y num num rdiv x num y num num rdiv x num y num num rdiv n num x real real rdiv x real n num real rdiv x num n num num real x num real size x T num stretch x num y num num stretch x num y num num sub x num y num num sub x num y num num sub x num y num num sum x num num 1999 Deloitte amp Touche Bakkenist ExSpect ExSpect User Manual utils the minimum of x utils x basic x mod y utils zmodylze x utils each element of x replaced by its value modulo y basic x y utils z ylzex utils real n x utils n x utils each element of x multiplied by y utils real x converted to num with a certain precision basic real x converted to num with precision y basic str x converted to num basic the numerator of a r
2. del x T y T ST basic y x x is deleted from the set y elt x T y ST bool basic x e y ins x T y T ST basic y union x insert x into y isect x T y ST ST basic x intersect y intersection max x num num utils z ze x and forall y e x z gt y maximum of set x 1999 Deloitte amp Touche Bakkenist ExSpect is a registered trade mark of ASPT 81 Deloitte amp Touche Bakkenist AN max x real real min x num num min x real real mod x num y num num mult x num y num num mult x real y real real pil x T2 S T pi2 x T gt lt S S pick x ST T rdiv x num y num num rdiv x real y real real rest x ST ST sdiff x ST y T ST size x T num sub x num y num num sub x real y real real subset x T y ST bool sum x num num sum x real real union x T T union x T y T T 5 8 Statistical functions ExSpect User Manual utils z ze x and forall y x z gt y maximum of set x utils z ze x and forall y x z lt y minimum of set x utils z ze x and forall y x z lt y minimum of set x utils zmodylze x utils z ylzex utils z ylze x utils yl y e T and exists ze S y gt lt z eE x utils zi ze S and exists y T y gt lt z e x basic arbitrary though deterministic element from X utils z y
3. Hzer served start service oi car_arrived end service car_drives on car_refueled Figure 5 System petrol_service_station After arrival in the service station a car will enter the queue when there is enough room for it otherwise it will drive on These two possible outcomes of the decision are modelled by the channels queue and car_drives_on see Figure 5 The decision is modelled by the processor decide The processors start_service and end_service model the beginning and the ending of the service When a car is waiting and the pump is free the processor start_service fires The car is moved from the queue to the channel being served When the service 1s ready the transition moves the car to the output channel car refueled o 1999 Deloitte amp Touche Bakkenist ExSpect is a registered trade mark of ASPT 20 Deloitte amp Touche Bakkenist AN Adding types ExSpect User Manual To add the channels do the following 1 In the submenu Add of the menu Object select Channel or use the channel button Oh 2 Move the mouse pointer over the gas station system window The cursor will change into the symbol for a channel 3 Click the left mouse button at the place you want to put the channel 4 Double click the new channel A property window appears 5 In the Name box type queue 6 Choose OK Repeat this for the channel pump free and being served To make the definition of the channels com
4. So 1 125 2 1 gt gt 1s a value of num num but lt lt 1 1 gt gt 1 2 is not Note that the second value does have type num num The first value also has type num gt lt num since any value of num gt num is also a value of num gt lt num We say that num gt num is stronger than num num The mapping operator can be used to model arrays num gt A can be used to represent an A array with elements lt lt 1 a4 lt lt 2 ao gt gt This is an alternative for the list A operator When sequential access only is needed the list approach is preferred but for random access the type num gt A is more profitable For combinations of the gt lt and gt operator it is advised always to use brackets to indicate the order Record types are constructed by means of attribute identifiers If lq lo are identifiers then H A l2 A is a record type Its values are for example 4 a lo a The type constructor and value constructor thus look the same in this case This 1s like the record construction in programming languages The order of the attributes 1s not important for example a num b str and b str a num denote the same record type and the values a 4 b a and b a a 4 denote the same record value within this type o 1999 Deloitte amp Touche Bakkenist ExSpect is a registered trade mark of ASPT 39 Deloitte amp Touche Bakkenist AN Type
5. gt 100 1000 gt gt The functional part of ExSpect is about defining stores channels and processors Stores and channels are defined by attaching types to them A type represents a set of values Processors are defined by attaching value expressions or terms to them A term represents a value which may depend upon some parameters We give an example the system FINANCE depicted in the figure below 1999 Deloitte amp Touche Bakkenist ExSpect is a registered trade mark of ASPT 34 Deloitte amp Touche Bakkenist AN ExSpect User Manual credit Y 4769 total subtract Figure 1 Finance system The channels credit debit and the store total are all typed with the basic type num numeral Non basic types are constructed from simpler types by means of type constructors for example num num numeral pair or name str salary num a record or tuple A type definition consists of an identifier the defined type and a type its definition The identifier can then be used in types instead of its definition Type expressions are types with variables They are used in signatures to describe the behaviour of functions The processors in figure 1 are both installations of the processor book with the following definition Connections amount in num total store num Pre amount O Val fun parameters kind val str o 1999 Deloitte amp Touche Bakkenist ExSpect is a regis
6. num str Hence T T T is a signature for all types T This is the meaning of the signature T T5 T where T is a type variable Functions with signatures containing type variables are called polymorphic o 1999 Deloitte amp Touche Bakkenist ExSpect is a registered trade mark of ASPT 43 Deloitte amp Touche Bakkenist ExSpect User Manual In the following table we give some standard polymorphic functions The type variables used are T and S Even polymorphic functions can be overloaded as in the last example name signature examples eq T Tbool a a true 11 21 false cond bool T T T iftruethen6else7fti 6 elt T Tbool 2 elt 1 3 5 false pick T9T pick 0 0 union T S TST 1 2 union 3 1 2 3 pil T gt lt SHT pil lt lt 3 a gt gt 3 pi2 T gt lt SS pi2 lt lt 3 a gt gt a dom T gt S T dom l 5 gt gt lt lt 2 7 gt gt 1 2 rng T gt S S rng 1 5 gt gt lt lt 2 7 gt gt 5 7 apply T 55 TS pes c o des 7 T gt S T S lt lt 1 5 gt gt lt lt 2 7 gt gt 1 2 5 7 ins T T T 4 ins l4 215 l4 4 2l ins T ST 4ins 2 4 2 4 4ins 3 2 2 3 4 head xT T head lt l4 4 21 4 strstr head Gee G name signature examples tail xT T tail l4 4 2 15 lt l4 2 gt strstr tail Gee ee cat xT T T lt 14 4I cat lt I2I gt l4 4 2I str strstr Oh cat boy Oh boy Ty
7. x basic y x x is deleted from the set y basic the denominator of a rational number basic x div y truncated utils domain of x basic x y utils x occurs in y basic x 2 y stat a random number erlang utils 1s n even basic e x basic falsehood utils x o y function composition utils fractional part of x utils fractional part of x utils x pick x x without the element pick x utils x with the last member removed stat draw from a gamma distribution with mean I k and variance l k 2 basic x y greatest common divisor utils x gt y utils x gt y utils x gt y utils x gt y basic first char in string x basic the first member of x utils x y logical equivalence utils x y logical implication basic y union x j insert x into y basic y with x added as head basic zl z dom x and x z y inverse is a registered trade mark of ASPT 69 Deloitte amp Touche Bakkenist AN inv x T gt S y S T isect x T y ST ST isint x num bool isint x str bool isnum x str bool isreal x str bool last x T T Icat x num gt T y num gt T num gt T Icons x num gt T y T num gt T le x num y num bool le x real y real bool lempty x num gt T bool Ifront x num gt T num gt T lhead x num T T list x T T llast x num gt T T In x real real In
8. y T num gt T adt append y at the back of list x Itail x num gt T num gt T adt list x without the first member Itobag x num gt T T gt num adt list x converted to a bag 1999 Deloitte amp Touche Bakkenist ExSpect is a registered trade mark of ASPT 86 Deloitte amp Touche Bakkenist AN 5 14 Bag functions ExSpect User Manual This section shows the bag functions of the module adt atobag x num gt T T gt num badd x T gt num y T T gt num badd x T T gt num bdel x T gt num y T T gt num bdiff x T gt num y T gt num T gt num bempty x T gt num bool bins x T gt num y T T gt num bisect x T gt num y T gt num T gt num bjoin x T gt num y T gt num T gt num bjoin x T gt num T gt num bmax x num gt num num bmin x num gt num num bnull void gt num bocc x T gt num y T num bpick x T gt num T bproj x T 2num y T T gt num brest x T gt num T gt num bsize x T gt num num bsum x num gt num num btoset x T gt num ST bunion x T gt num y T num T gt num bunion x T gt num T gt num Itobag x num gt T T gt num stobag x T T gt num subbag x T gt num y T gt num bool 1999 Deloitte amp Touche Bakkenist ExSpect adt array x converted to a bag adt bag x with all elements of y added adt bag of all elements occurring in the sets in
9. 2 3 Ix gt 3 false T gt bool gt T set x 1 2 3 Ix gt 1 2 3 sum T gt num num sum x 1 2 3 x 1 9 union T gt S S union x 1 2 3 l x x 1 1 2 3 4 Note that union is an overloaded polymorphic function The term set x A E can also be written x A E because of the association of set with the symbol 1999 Deloitte amp Touche Bakkenist ExSpect is a registered trade mark of ASPT 48 Deloitte amp Touche Bakkenist AN Function definitions ExSpect User Manual We tabulate some terms with their mathematical counterpart Here x is a variable Ex a term containing x Py a predicate containing x Ny a numerical term containing x Sy a set term containing x and A a finite set We added the max and min quantors that have the same signature as sum ExSpect math x AIEx x Ex lx A rng x AIPy Pxlx e A all x AIPx Vx A Px any x AIPx dx A Px set x AIPX xlx AA Px sum x AINx Yye ANx max x AINx MAXxe ANx min x AINx MINxe ANx union x AISy Uxe ASx rng x set x AIPx JIEx Ex X A A Px Note the last element where two quantors are combined Like type definitions function definitions are made by attaching a name to a term A function definition must be accompanied by its signature so its parameter variables and their types and its result type must accompany the body term A term without parameters can be defined too giving a val
10. Schoonhoven 1997 in Dutch J Desel and J Esparza Free choice Petri nets volume 40 of Cambridge tracts in theoretical computer science Cambridge University Press Cambridge 1995 K M van Hee Information System Engineering a Formal Approach Cambridge University Press 1994 K Jensen Coloured Petri Nets Basic concepts analysis methods and practical use EATCS monographs on Theoretical Computer Science Springer Verlag Berlin 1992 K Jensen and G Rozenberg editors High level Petri Nets Theory and Application Springer Verlag Berlin 1991 Pallas Athena Protos User Manual Pallas Athena BV Plasmolen The Netherlands 1997 J L Peterson Petri net theory and the modeling of systems Prentice Hall Englewood Cliffs 1981 W Reisig Petri nets an introduction volume 4 of Monographs in theoretical computer science an EATCS series Springer Verlag Berlin 1985 S M Ross A course in simulation Macmillan New York 1990 Software Ley COSA User Manual Software Ley GmbH Pullheim Germany 1996 o 1999 Deloitte amp Touche Bakkenist ExSpect is a registered trade mark of ASPT 89
11. User Manual utils x real n utils each member of x divided by y utils each member of x divided by y basic num x converted to real basic str x converted to real basic x pick x utils x l y restricted to utils string x in reverse order utils list x in reverse order stat a random number between a and b utils range of x utils does x occur in y utils tail of y from first occurrence of x in y basic x Vy basic yl y e T and x y basic the set of members of x basic x basic sum y x 1 number of elements of x utils number of members of x basic square root of x adt set x converted to a bag basic x converted to string basic x converted to string utils are the first n characters of strings x and y the same utils list containing all members of z x lt z lt yj utils z x az y utils length of string x stat a random number student basic x y utils z ylzex is a registered trade mark of ASPT 73 Deloitte amp Touche Bakkenist AN sub x real y real real sub x real y real real sub x num y num num sub x real y real real sub n num x real real sub x real n num real subbag x T gt num y T gt num bool subset x T y ST bool sum x num num sum x T num num sum x real real sum x T gt real real sum x num num sum x real real tail x str
12. a registered trade mark of ASPT 40 Deloitte amp Touche Bakkenist AN ExSpect User Manual 3 2 Lesson 2 Functions and terms Functions Terms are atoms constants variables or constructions out of these by means of functions and quantors We first concentrate on functions Functions transform input values into a result value Function applications are terms involving the function symbol and simpler argument terms For instance the term sin 3 14 signifies the application of the function sin sinus onto the term 3 14 the evaluation of this term results in a term of type real close to 0 0 The term 1 2 signifies the application of add addition onto 1 and 2 the evaluation result is 3 The term a 2 signifies the application of add addition onto a and 2 the evaluation result depends upon the value that 1s substituted for a Signature Which input values of a function are accepted and which result value is given is determined by the function s signature The signature of sin is real for input and real for result of add it is num num for input and num for result We represent these signatures by real real and num num num respectively Standard functions ExSpect has a large number of standard functions From them new functions can be defined We first describe some standard functions and their applications Then we discuss quantors Finally we describe how new functions can be defined Simple functions A simple functio
13. amp Touche Bakkenist AN ExSpect User Manual E CC ee E Ce i a Coc Ee pe Cd Eje pe eere roseesenennr Er p essen sone Eje pe Ce Eje jer rese ramo i e Zee Figure 6 Simulation results When the differences between the results in the subruns are high it means that the results are unreliable Because in this case for all subruns the average is near 7 minutes we can conclude that the throughput time is indeed about 7 minutes With this information it is however impossible to give an answer to the question whether waiting of ten minutes or more occur We need the results of the measure count_cars_driven_on when we want to know how many cars had to drive on in comparison to the number of cars that could be serviced To view these results 1 Double click the table object A Dashboard Objects Properties window appears 2 In the Place box select the channel main tel doorrijders tmeasurement cumm results 3 Choose OK Size the table 1f necessary 1999 Deloitte amp Touche Bakkenist ExSpect is a registered trade mark of ASPT Deloitte amp Touche Bakkenist AN ExSpect User Manual Figure 7 shows an example of the results Because the cars are not serviced the throughput time and the variance are 0 When the column arrivals is compared to this column in Figure 6 we can see that indeed about 8 of the cars have to drive on This means that the question whether drivers evade the ru
14. and money goods and information flows you can use ExSpect to determine the service level of your organisation ExSpect offers the potential for every conceivable kind of simulation and so helps you reach decisions on cost reductions and large scale infrastructure investment program s ExSpect has a full graphic user interface and a sound formal basis developed in close co operation with Eindhoven University of Technology since 1980 ExSpect users are able to build executable models with ease and speed Changing developed models is an even simpler matter since a library of building blocks 1s automatically generated during development An advantage of ExSpect is that it 1s possible to use application libraries specifically prepared for particular fields Libraries are available for workflow logistics administrative processes and more specific business situations Deloitte amp Touche Bakkenist offers you a helpdesk for answering your questions related to the tool and modelling A total service package including various standard and specially tailored courses plus a workshop is available When desired staff from Deloitte amp Touche Bakkenist will assist you in developing your business applications 1999 Deloitte amp Touche Bakkenist ExSpect is a registered trade mark of ASPT 3 Deloitte amp Touche Bakkenist AN This manual ExSpect User Manual This manual starts with two tutorial cases to get familiar with the t
15. answer we need to add another dashboard object to the dashboard This time we choose the Textbox dashboard object 1 Press the Textbox button E and move the mouse pointer in the Dashboard window Now press the left mouse button and a Texbox will appear 2 Press the connector button 3 Select the channel answer in the System Definition window Select the Textbox in the Dashboard window Now the Textbox will show the contents of answer Note the name of the Texbox 1s automatically changed to answer o 1999 Deloitte amp Touche Bakkenist ExSpect is a registered trade mark of ASPT 17 Deloitte amp Touche Bakkenist A ExSpect User Manual 2 Tutorial 2 Simulating a petrol service station Introduction In this tutorial the case of a petrol service station is used to explain the basic principles of simulation with ExSpect Simulation is an analysis technique that mimics reality by using a model It enables experimentation with a model of the reality This 1s useful when real experiments are expensive or dangerous Case description A taxicab company has its own petrol service station where the taxi drivers can refuel their cars A taxi driver that needs to refuel his car 1s obliged to drive to this service station The station has a queue that can hold three cars When there is no room in the queue the taxi driver must drive on and go to another service station It takes between 2 and 5 minutes to refuel a car and
16. denote abortion is a registered trade mark of ASPT 85 Deloitte amp Touche Bakkenist AN ExSpect User Manual tovoid x T void utils x converted to void 5 12 Array functions This section shows the array functions of the module adt adel x num gt T y num num gt T adt array x without the y th member aelement x num gt T y num T adt x y value of the y th member of array x aempty x num gt T bool adt is x an empty array aindex x num gt T y T num adt i dom x x i y ains x num gt T y num z T num gt T adt array x with y z inserted ains x num gt T y num z num gt T num gt T adt array x with array z inserted at position y anull num gt Void adt the empty array asplit x num gt T y num num 2T num T adt split array x at index y aswap x num gt T y num z num num gt T adt array x with values at y and z interchanged 5 13 List functions This section shows the list functions of the module adt Icat x num gt T y num gt T num gt T adt concatenation of lists x and y Icons x num gt T y T num gt T adt append y in front of list x lempty x num gt T bool adt 1s x an empty list Ifront x num gt T num gt T adt list x without the last member lhead x num gt T T adt first member of list x Inull num gt void adt the empty list lreverse x num gt T num gt T adt reverse of list x Isnoc x num gt T
17. for recursive definitions that refer to themselves As an example we define the size of a set name size parameters x T result type num body if x then 0 else 1 size rest x fi Recursive definitions must be used with care since they may lead to non termination We give an example of a dangerous recursive definition name div parameters x num y num result type num body if x lt y then x else 1 div x y y fi Evaluating the function 2 div 1 will not terminate As an exercise try to improve upon this definition In the majority of cases recursion can be replaced by quantor definitions The body in size could have been sun t x 1 Consider the function that extracts the addresses from a set of client records name addresses parameters x name str addr str result type X str body if x then else pick x addr union addresses rest x fi o 1999 Deloitte amp Touche Bakkenist ExSpect is a registered trade mark of ASPT 52 Deloitte amp Touche Bakkenist AN Exercises Types and sets Functions and mappings ExSpect User Manual Much more comprehensible concise and efficient is the body rng t x t addr 1 Define a function avg that computes the average of two numbers and also of a set of numbers Make 4 overloaded definitions for 2 nums for num for 2 reals and for real 2 Define a function dommax of signature T gt num gt T that selects
18. member incremented by y adel x num gt T y num num gt T adt array x without the y th member aempty x num gt T bool adt is x an empty array aelement x num gt T y num T adt x y value of the y th member of array x aindex x num gt T y T num adt i dom x x i y ains x num gt T y num z T num gt T adt array x with y z inserted ains x num gt T y num z num gt T num gt T adt array x with array z inserted at position y all x T gt bool bool utils forall y e dom x x y and x bool y bool bool utils x and y logical and anull num void adt the empty array any x T gt bool bool utils exists y dom x x y apply x T gt S y T S basic x y mapping application apply x T gt S y T S utils x z z ey asplit x num gt T y num num gt T gt lt num gt T adt split array x at index y aswap x num gt T y num z num num gt T adt array x with values at y and z interchanged atobag x num gt T T gt num adt array x converted to a bag 1999 Deloitte amp Touche Bakkenist ExSpect is a registered trade mark of ASPT 67 Deloitte amp Touche Bakkenist AN badd x T gt num y T T gt num badd x T T gt num bdel x T gt num y T T gt num bdiff x T gt num y T gt num T gt num bempty x T gt num bool bernouilli p real seed real real binomial n real p real seed real real bins x T gt num
19. they are bound to fixed values functions Pins are dynamic the values they contain may vary during the execution of the topmost system 1999 Deloitte amp Touche Bakkenist ExSpect is a registered trade mark of ASPT 56 Deloitte amp Touche Bakkenist AN ExSpect User Manual Processor activation A processor is activated when the channels linked to its input pins contain a token combination that satisfies the precondition Upon activation the activating tokens are consumed Their values are bound to the corresponding parameter variables as are the store values According to the specified statements tokens are produced for the channels linked to the output pins and the store values are updated In a conditional statement the then part is executed if the condition predicate evaluates to true the else part is executed if it evaluates to false A missing else part means that the statement is skipped in this last case The skip statement performs no actions An assignment statement causes the creation of an output token for output pins or an update of the store value for store pins The created token becomes available after d time units where d 1s the corresponding value of the delay term If the delay term is absent d 0 More assignments for the same output pin are allowed in this case several tokens are produced for the same channel More assignments for the same store pin are not allowed Delayed assignments for s
20. to create them from scratch For this use of ExSpect as a high level programming language this tutorial is destined The part that deals with these aspects 1s called the functional part of ExSpect It resembles typed functional programming languages hence this qualification The most striking difference of the ExSpect language compared to ordinary third generation programming 1999 Deloitte amp Touche Bakkenist ExSpect is a registered trade mark of ASPT 33 Deloitte amp Touche Bakkenist AN Stores channels and processors ExSpect User Manual languages are the absence of the sequencing semicolon operator In the C language for example introducing an auxiliary variable help and executing the following statements performs interchanging the values of variable x and y usually help x x y y help In ExSpect this is done by the following simultaneous assignment X lt Y y lt X It is assumed that x y are stores here In a simultaneous assignment the variables stores retain their value until the complete assignment has been executed The order in which they are given is of no effect Another difference is that ExSpect allows assignments of very complex datatypes in one stroke for instance the assignment S lt x stretch 0 100 x x fills the store or channel s with a table giving the squares for the numbers 0 up to 100 0 0 gt gt 1 1 gt gt 2 4 gt
21. trade mark of ASPT 37 Deloitte amp Touche Bakkenist AN Void Constructed types and their values Sets Lists ExSpect User Manual So 2 and 3 14159 are reals whereas 2 and 314159 100000 are nums Manipulation with reals is faster than with nums but at a price reals are approximated So 2 5 2 5 5 need not necessarily hold the result might be for example 4 9999999999761 The approximation made depends on the hardware platform used There is also a maximum real exceeding this maximum gives rise to errors similar to division by zero There is a fifth basic type void which has no constants It is used in type constructions to denote some degenerate values To construct new types we use our type constructors gt lt gt and the record operator Basic types and type constructors represent sets of constructed non atomic values In the sequence we assume that A B A are types The type A contains finite sets of values from A Enclosing their elements in braces represents these sets So num contains for example the values the empty set 1 2 5 3 3599 333 and so on The value constructor is here Note that the empty set belongs to all set types This fact is reflected by giving it the degenerate type void Itis not allowed to put values from different types within the same set so for example 1 2 0 1s an illegal value Note that bool and false true ha
22. x adt bag x with one element y deleted adt bag x minus all elements of bag y adt is x an empty bag adt bag x with element y inserted adt biggest bag both contained in x and y bag intersection adt bag of all elements of x and y join adt bag of all elements of all bags in x join adt maximum greatest element of bag x adt minimum smallest element of bag x adt the empty bag adt number of times y occurs in bag x adt an arbitrary though deterministic element from bag x adt projection of bag x onto y adt bag x without the element bpick x adt number of elements in bag x adt sum of all elements of bag x adt bag x converted to a set adt smallest bag containing x and y bag union adt smallest bag containing all bags of x bag union adt list x converted to a bag adt set x converted to a bag adt 1s bag x contained in y bag subset is a registered trade mark of ASPT 87 Deloitte amp Touche Bakkenist AN ExSpect User Manual 6 Bibliography References For a good introduction to the modelling of systems and processes in terms of Petri nets the user is referred to AA Kea96 and AH97 Both books are in Dutch Other goods introductions to Petri net modelling are given in Pet81 Jen92 and Re185 The tools described in Pal97 and SL96 export script files which can be imported by ExSpect For more background information on modelling and simulatio
23. x multiplied by y utils real x converted to num utils x gt 0 utils x y basic x y utils z ylze x utils real n x utils x real n utils each member of x divided by y basic num x converted to real basic str x converted to real basic x basic square root of x basic x converted to string basic x y utils z ylze x utils real n x utils x real n utils each member of x subtracted by y utils sum y x y utils sum y dom x x y utils the sum of all members of x is a registered trade mark of ASPT 79 Deloitte amp Touche Bakkenist AN 5 4 String functions ExSpect User Manual This section shows all string functions of the modules basic and utils cat x str y str str chop x str n num str head x str str isint x str bool isnum x str bool isreal x str bool match x str y str bool num x str num parse y str symbols str num gt str parse y str num gt str real x str real rev x str str scan x str y str bool scanrest x str y str str str x num str strncmp x str y str n num bool strlen x str num tail x str str 1999 Deloitte amp Touche Bakkenist basic x concatenated with y utils string x reduced to its first n characters basic first char in string x utils is x an integer basic is x a num basic 1s x a real utils 1s x head of
24. A random store is a store that always contains a new random number To add the random store do the following 1 In the submenu Add of the menu Object select Random Store Tip use the random store button E 2 Move the mouse pointer over the gas station system window The cursor will change into the symbol for a random store 3 Click the left mouse button at the place you want to put the store 4 Connect the store with the processor start_service Now the definition of the processor start_service can be added Put the following definition in the processor start_service number of cars in queue number of cars in queue 1 being served queue delay uniform 2 0 5 0 random The keyword delay in the last statement specifies that the token becomes available in the channel filling tank only after a certain amount of time This models the time it takes to refuel the car In the next chapter this will be explained in more detail To finish the model add the following definition for the processor end service o 1999 Deloitte amp Touche Bakkenist ExSpect is a registered trade mark of ASPT 2b5 Deloitte amp Touche Bakkenist AN Running a simulation ExSpect User Manual pump free lt pump car refueled being served The model that has been created in the previous paragraphs can now be executed To start the simulation mode do the following 1 In the Tools menu choose Simulate or press th
25. Deloitte amp Touche Bakkenist A Management amp ICT EB x Spe ct Consultants Telephone 31 20 495 23 23 Telefax 31 20 495 23 45 Wisselwerking 46 1112 XR Diemen The Netherlands User Manual 1999 Deloitte amp Touche Bakkenist ExSpect is a registered trade mark of ASPT 1 Deloitte amp Touche Bakkenist AN Contents 1 Tutorial 1 Building a phone book ExSpect User Manual 2 Tutorial 2 Simulating a petrol service station 3 The language 3 1 Lesson 1 Types and values 3 2 Lesson 2 Functions and terms 3 3 Lesson 3 The dynamic part 4 Syntax 5 Function list 5 1 Boolean functions 5 2 Numerical functions 5 3 Real functions 5 4 String functions Tuple functions 5 6 Product functions 2 Set functions 5 8 Statistical functions 5 9 List functions 5 10 Mapping functions 5 11 Void functions 5 12 Array functions 5 13 List functions 5 14 Bag functions 6 Bibliography 1999 Deloitte amp Touche Bakkenist ExSpect is a registered trade mark of ASPT 18 31 37 4 55 63 67 74 76 78 80 81 81 8l 82 83 85 85 86 86 87 88 Deloitte amp Touche Bakkenist AN Introduction ExSpect Deloitte amp Touche Bakkenist ExSpect User Manual ExSpect Executable Specification Tool is a powerful business tool giving organisations the ability to model monitor and analyse business processes effectively and efficiently By tracking workloads
26. LV 1 expr 1 8 expr stype type stype type stype o 1999 Deloitte amp Touche Bakkenist ExSpect is a registered trade mark of ASPT 65 Deloitte amp Touche Bakkenist AN stype const num real string id ExSpect User Manual id type Y stype 1d type T num real string du II 0 9 O 0 70 9 fe L2 CO 69 D mem pan ye a Z A Z C a 2 SA Z SO 9 _ 1999 Deloitte amp Touche Bakkenist ExSpect is a registered trade mark of ASPT 66 Deloitte amp Touche ina ExSpect User Manual 5 Function list Here all functions defined in the modules basic utils stat and adt are listed alphabetically For every function the module is given in which the function is defined and a short hint as to what the result will be of an invocation of that particular function abort void basic value to denote abortion abs x num num utils x absolute value add x num y num num basic x y add x num y num num utils z ylzex add x real y real real basic x y add x real y real real utils z ylzex add n num x real real utils real n x add x real n num real utils x n add x num y num num utils x with each member incremented by y add x real y real real utils x with each
27. Spect is a registered trade mark of ASPT 60 Deloitte amp Touche Bakkenist AN ExSpect User Manual Consider the following definition of the Fibonacci function name fib parameters x num result type num body if x lt 2 then 1 else fib x 1 fib x 2 fi Evaluating for example fib 5 means going through the following steps fib 5 fib 4 fib 3 fib 3 fib 2 fib 2 fib 1 fib 2 fib 1 fib 1 fib 0 fib 1 fib 0 1 fib 1 fib 0 1 1 1 1 1 1 14 146 8 We see that in the above process fib 3 1s evaluated twice and fib 2 three times When evaluating fib for higher values this gets worse and worse thus causing bad performance It would be less inefficient to evaluate fib 5 as follows fib 5 gt 1 fib 5 0 fib 4 gt fib 4 1 fib 3 2 fib 3 1 fib 2 gt 3 fib 2 42 fib 1 5 fib 1 23 fib 0 8 o 1999 Deloitte amp Touche Bakkenist ExSpect is a registered trade mark of ASPT 61 Deloitte amp Touch Bakkenist Scope Exercises AN ExSpect User Manual By creating a subordinate function with more parameters this can be achieved The body of fib becomes fib2 x 1 0 where fib2 with num parameters x y z is defined with the body If x lt 2 then y z else fib2 x 1 y z y fi The function fib2 has no use except in the context of the fib function so it 1s natural to define it as local function of fib Local functions can be nested but it is not advised to u
28. accepts one or more parameters of type T and yield a result of type T The projection functions _ I accept a parameter of any type of the form T and yield a result of type T The record update function accepts two parameters of type l4 T1 and m1 S1 respectively such that common labels are matched to the same types 1 e if 2 m4 then T4 S1 The result type is the record type that joins the parameter types o 1999 Deloitte amp Touche Bakkenist ExSpect is a registered trade mark of ASPT 45 Deloitte amp Touche Bakkenist A Erroneous function applications Exercises ExSpect User Manual In writing function application terms three kinds of errors may occur The first ones are syntax errors due to ill matched brackets misspellings and the like The second are errors against the signature for instance in the term 1 2 union 5 0 or 5 02 5 Both kinds of errors are discovered during translation and reported by a syntax error or type unknown error message The third are runtime errors which are detected during execution only Examples are given in the table below runtime error explanation 1 0 division by zero head head tail of empty string pick pick on empty set lt lt 1 2 gt gt lt lt 3 4 gt gt 2 invalid apply argument name Jan Q address invalid apply argument In these cases the non value abort is the evaluation result Of course nobody will write the above
29. at a random number negative exponential stat a random number normal utils not x logical not is a registered trade mark of ASPT 71 Deloitte amp Touche Bakkenist AN num x real num num x real y num num num x str num numerator x num num odd n num bool or x bool y bool bool parse y str symbols str num gt str parse y str num gt str PERT beta l real u real e real seed real pil x T gt lt S T pil x T gt lt S ST pi2 x T gt lt S S pi2 x T gt lt S S pick x T T poisson m real seed real real pos x num bool pos x real bool pow x num y num num pow x real y real real prod x T y S T gt lt S random seed real real rdiv x num y num num rdiv x num y num num rdiv x real y real real rdiv x real y real real rdiv n num x real real o 1999 Deloitte amp Touche Bakkenist ExSpect ExSpect User Manual utils real x converted to num with a certain precision basic real x converted to num with precision y basic str x converted to num basic the numerator of a rational number utils 1s n odd utils x or y logical or utils divides the string y in a list of substrings e g words that are separated by a delimiter in symbols utils divides the string y in a list of substrings e g words that are separated by a space or by the characters 1 stat draw from a beta distribut
30. at have driven on and the throughput time are interesting For every car the waiting time and the service time 1s measured The sum of these two numbers 1s the throughput time To view the simulation results we add some dashboard objects to the dashboard With the dashboard the simulation can be monitored 1 In the Simulation menu select Show Dashboard or press the dashboard button ED 2 Push the Table button Move the mouse pointer over the Dashboard window The cursor will change into the symbol for a table dashboard object Click the left mouse button at the place you want to put the table object 5 Double click the new table object A Dashboard Objects Properties window appears 6 In the Place box select the channel main measure throughput time tmeasurement cumm results 7 Choose OK Resize the table if necessary Figure 6 shows an example of a table containing simulation results The table contains a row for every subrun The column arrivals shows the number of tokens that arrived 1n the measure which 1s the number of cars that have refuelled The column average contains the average throughput time of all tokens in the subrun This 1s the average time it took to refuel the cars in the subrun The column variance indicates the reliability of the average throughput time For the interpretation of the variance we refer to Ros90 1999 Deloitte amp Touche Bakkenist ExSpect is a registered trade mark of ASPT 28 Deloitte
31. ational number utils 1s n odd basic x gt 0 utils x y basic x y utils z ylze x utils real n x utils x real n utils each element of x divided by y basic num x converted to real utils number of elements in x utils list containing all elements of x y utils z x az 2y basic x y utils z ylze x utils each element of x subtracted with y utils sum y x y is a registered trade mark of ASPT 77 Deloitte amp Touche Bakkenist AN sum x T num num sum x num num 5 3 Real functions ExSpect User Manual utils sum y e dom x x y utils the sum of all members of x This section shows all functions with reals as a result type or as an argument in the modules basic and utils add x real y real real add x real y real real add n num x real real add x real n num real add x real y real real botint x real num cos x real real exp x real real frc x real real ge x real y real bool et x real y real bool le x real y real bool In x real real It x real y real bool max x real real max x real y real real max x T gt real real max x real real minus x real real min x real real min x real y real real 1999 Deloitte amp Touche Bakkenist ExSpect basic x y utils z ylze x utils real n x utils x n utils each e
32. book is a table with information about phone numbers In Table 1 an example of this information 1s given The phone book is a very simple example of an information system But nevertheless this example contains most ingredients that are relevant in larger systems Name Phone number Jack 020 2210922 Gary 39 227 644413 Mary 040 2471127 Frank 045 5678230 Patrick 01 518 2766261 Table 1 A user of a phone book can do four things e Look up a phone number e Add anew phone number to the phone book e Remove an existing phone number from the phone book e Change an existing number in the phone book 1999 Deloitte amp Touche Bakkenist ExSpect is a registered trade mark of ASPT 5 Deloitte amp Touche Bakkenist AN Getting started ExSpect User Manual Let s examine these four actions If a user searches a phone number s he has to enter a name The answer of the phone book will be the number belonging to this name If the name doesn t exist in the phone book the output of the phone book will be not found If the user wants to add a phone number s he has to enter a name and a phone number If a user wants to remove a phone number only the name belonging to the phone number has to be given To change a phone number a name and a phone number have to be given To keep this example simple we assume the following First of all phone numbers that are to be changed or removed are always in the
33. bool any x T gt bool bool apply x T gt S y T S apply x T gt S y T S dom x T gt S ST fcomp x T gt S y S gt R T gt R frest x S gt T S gt T inv x T gt S y S T inv x T gt S y S T max x T num num max x T real real min x T gt num num min x T gt real real restrict x T gt S y T T gt S rng x T gt S S set x T gt bool T sum x T gt num num sum x T gt real real that x T gt bool T tomap x T gt lt S T gt S upd x T gt S y T z S T gt S 5 11 Void functions This section shows all void functions abort void 1999 Deloitte amp Touche Bakkenist ExSpect ExSpect User Manual utils forall y e dom x x y utils exists y dom x x y basic x y mapping application utils x z ze y utils domain of x utils x o y function composition utils x pick x x without the element pick x basic z ze T and x z y inverse utils z ze T and x z y inverse utils max rng x utils max rng x utils min rng x utils min rng x utils x l y restricted to utils range of x basic yl y e T and x y utils sum y e dom x x y utils sum y e dom x x y utils z z e dom x and x z and forall y dom x and x y y 2z the only element in T that is true utils type casting of set of pairs to mapping basic update x with x y 2 z basic value to
34. bool bool any x T gt bool bool cond x bool y T z T T elt x T y ST bool elt x T y T bool eq x T y T bool even n num bool false bool ge x num y num bool ge x real y real bool gt x num y num bool et x real y real bool iff x bool y bool bool impl x bool y bool bool isint x num bool le x num y num bool le x real y real bool It x xnum y num bool It x real y real bool match x str y str bool ne x T y T bool not x bool bool odd n num bool or x bool y bool bool pos x num bool pos x real bool scan x str y str bool subset x T y ST bool true bool 1999 Deloitte amp Touche Bakkenist ExSpect ExSpect User Manual utils forall y e dom x x y utils x and y logical and utils exists y dom x x y basic if x then y else z condition basic x e y basic x occurs in y basic x 2 y utils 1s n even basic falsehood utils x gt y utils x gt y utils x gt y utils x gt y utils x y logical equivalence utils x gt y logical implication utils is x an integer utils x lt y utils x lt y utils x lt y utils x y utils is x head of y utils x y x not equal to y utils not x logical not utils 1s n odd utils x or y logical or basic x gt 0 utils x gt 0 utils does x occur in y utils x lt y bas
35. d in the following way 1 Double click the processor add 2 Enter the following text in the definition box of the processor definition window contents_phone_book lt entry_to_add ins contents_phone_book 3 Press OK to save and close the processor definition window 1999 Deloitte amp Touche Bakkenist ExSpect is a registered trade mark of ASPT L3 Deloitte amp Touche Bakkenist AN Processor change Processor remove ExSpect User Manual The processor change changes the number belonging to one of the names in the phone book Inserting a new changed entry and removing the old one from the phone book does this This is implemented in the following way 1 Double click the processor change 2 Enter the following text in the definition box of the processor definition window contents_phone_book lt entry_to_change ins set x contents phone booklx name entry to change name 3 Press OK to save and close the processor definition window The processor remove removes an entry with a given name from the phone book This 1s implemented in the following way 1 Double click the processor remove 2 Enter the following text in the definition box of the processor definition window contents_phone_book lt set x contents_phone_book x name entry to removel 3 Press OK to save and close the processor definition window Now the specification is finished and ready to be checked Clicking th
36. definitions Exercises ExSpect User Manual Type constructions can be given a name a type definition Names must obey the syntax for identifiers they must begin with an alphabetic character and may not contain spaces After its definition a newly defined type can be used in type constructions thus maybe creating more complex defined types So the order in which type definitions are given is important We show an example where a client file is defined The defined types are address and client in that order with the following constructions type name type from address street str city str zip str client nr num name str addr address The type client can be used to model for example a store containing client data 1 Which of the following examples represent correct values What is their type 2 56 7 abcd U 5 4 false true 4 UB lt lt 1 7 gt gt a l b lt lt lt lt 4 gt gt 1 gt gt 2 Try to define ExSpect types for the following kinds of data Give type definitions by choosing an appropriate name for them a single line error message the measured volume pressure and temperature of a gas a multi line ASCH document the results of the games played in a soccer league 3 Give the values in the types bool and boo gt lt bool Give the number of values in the types boo gt lt bool and bool gt bool 1999 Deloitte amp Touche Bakkenist ExSpect is
37. dt an arbitrary though deterministic element from bag x adt projection of bag x onto y adt bag x without the element bpick x adt number of elements in bag x adt sum of all elements of bag x adt bag x converted to a set adt smallest bag containing x and y bag union adt smallest bag containing all bags of x bag union basic x concatenated with y basic the concatenation of x and y stat a random number X squared utils string x reduced to its first n characters is a registered trade mark of ASPT 68 Deloitte amp Touche Bakkenist AN cond x bool y T z T T cos x real real del x T y T T denominator x num num div x num y num num dom x T gt S ST elt x T y T bool elt x T y T bool eq x T y T bool erlang m real k real seed real real even n num bool exp x real real false bool fcomp x T gt S y S gt R T gt R frc x num num frc x real real frest x S gt T S gt T front x T T ecammaj I real k real seed real ecd x num y num num ge x num y num bool ge x real y real bool gt x num y num bool et x real y real bool head x str str head x T T iff x bool y bool bool impl x bool y bool bool ins x T y T ST ins x T y T T inv x T gt S y S ST 1999 Deloitte amp Touche Bakkenist ExSpect User Manual basic if x then y else z condition basic
38. e Translate button does this fall This will first save the specification and then check it for mistakes If we do this the following translation error will appear store phone_book contents_phone_book empty init value By double clicking this error with the left mouse button the Store Definition window will open Here we see that we have forgotten to give our store contents phone book an initial value We choose that the initial value of contents phone book is empty Therefore we insert in the Initial Value box Now we translate our specification again and we see that there are no error messages left o 1999 Deloitte amp Touche Bakkenist ExSpect is a registered trade mark of ASPT 14 Deloitte amp Touche Bakkenist A ExSpect User Manual The use of the phone book Adding entries to the phone book Adding a table dashboard object In the following we describe the use of our information system But before we can do this we have to start the simulation by pressing the simulation button 3 This will initiate three consecutive actions first the specification will be saved then checked and finally the simulation will be started We start by entering several entries into our phone book Select the place entry to add Press the right mouse button and select Add Token from the pop up menu Enter a valid entry in the Add Token window and press the Apply button For this example we have entered the first thre
39. e number in number of cars in queue had to be increased The following steps achieve this 1 Double click the processor decide 2 In the definition box type the following if number of cars in queue lt 3 then queue car arrived number of cars in queue lt number of cars in queue 1 else car drives on car arrived fi 3 Choose OK An assignment statement is used to move a token from one channel to another In the ExSpect language an assignment statement looks as follows Output channel Input channel For example the statement queue car arrived in the second line of the processor means that a token is moved from the channel car arrived to the channel queue Another language feature that is used 1s the if statement that looks like this if expression then alternativel else alternative2 fi o 1999 Deloitte amp Touche Bakkenist ExSpect is a registered trade mark of ASPT 24 Deloitte amp Touche Bakkenist AN Adding a random store ExSpect User Manual When expression evaluates to true alternative is performed otherwise alternative2 In the example it is used to make the decision The next chapter explains the ExSpect language in more detail From the case description we know that it takes between 2 and 5 minutes to refuel a car We assume that this service time has a uniform distribution To model this random behaviour the processor start service is connected with a random store
40. e rows from Table 1 After this pressing the Close button closes the Add token window Next we start the simulation by pressing the Play button gt We see that the new entries are added to contents_phone_book Now we want to check if the right entries are added to contents_phone_book Adding a dashboard object is the best way First activate the dashboard window by pressing the Dashboard button EM Press the Table button E and move the mouse pointer in the Dashboard window Now press the left mouse button and an indication of a table will appear Double click the indication of the table with the left mouse button and the Dashboard Object Properties window appears First we give a name to the dashboard object by entering a name in the Name box 1999 Deloitte amp Touche Bakkenist ExSpect is a registered trade mark of ASPT l5 Deloitte amp Touche Bakkenist AN Changing entries in the phone book Removing entries from the phone book ExSpect User Manual 5 Then we enter a place or store of which we want to see the contents in the place box In our case this is Phone_book contents_phone_book System name dot name of the channel store Click OK to save and close the Dashboard Object Properties window In the dashboard object the contents of contents phone book can be seen Now that these three entries are entered we would like to change one of them So suppose Gary moves and gets a
41. e simulation button amp An Incompleteness Errors window appears containing an error message about an empty initial value We forgot to enter an initial token value for the store number of cars in queue This error must be resolved first 1 Double click the error message The store definition window for the store number of cars in queue appears 2 In the Initial Value box type 0 3 Choose OK Now we can start the simulation Push the simulation button When the specification 1s free of errors a System Animation window will appear for the system main 2 Double click the system gas station to get its System Animation window 3 n the menu Simulation select Play or press the Play button In the System Animation window you can see the tokens flow through the process The simulation time is shown in the right bottom corner of the screen If you run the simulation long enough it will halt automatically o 1999 Deloitte amp Touche Bakkenist ExSpect is a registered trade mark of ASPT 26 Deloitte amp Touche Bakkenist AN Dashboard objects ExSpect User Manual It is not directly observable whether the queue is full or not We will add a traffic light to the picture to solve this Press the Halt button a The simulation will pause Press the Animation Dashboard object button mj 3 Move the mouse pointer over the gas station system animation window The cursor will change into the symbol for a
42. en In figure 1 the process we are going to design 1s given But before we start defining this phone book we recall the informal description earlier entry to add add number to search contents phone book e9 entry to remove search remove change answer entry to change Figure 1 The user can initiate four actions searching adding removing and changing Therefore 1999 Deloitte amp Touche Bakkenist ExSpect is a registered trade mark of ASPT 7 Deloitte amp Touche Bakkenist AN Placing stores ExSpect User Manual channel answer Click with the left mouse button on the Channel button O Click with the left mouse button in the System Definition window at the place you want to put the channel Now a channel with an automatically generated name will appear We repeat 1 and 2 until we have five channels in the definition window By double clicking a channel with the left mouse button the Channel Definition window will open In the Name box of this window we can give each channel an appropriate name use the names we have chosen above Press the OK button to save and close the Channel Definition window The phone book has to keep information about the phone numbers and names that are put into it Therefore we have to define a store Click with the left mouse button on the Store button E Click with the left mouse button in the System Definition window at the p
43. er Manual The body of the mapping update function could also have been y union set t x not pi1 t elt dom y This example needs some study since many functions are combined An example of the mapping update 1 22 3 4 gt gt upd lt lt 3 5 gt gt yields 1 2 gt gt 3 5 gt gt The update of a mapping at a single point as 1n the above example is used frequently an extra overloaded definition has been added as follows name upd parameters x T gt S y T z S result type T 5S body x upd lt lt y z The above definition is not accepted by the translator since it cannot perceive that the term y z gt gt is a mapping Instead it is typed with T gt lt S and a function upd with signature T gt S gt T gt lt S is not found So an error message type of upd unknown is issued This problem can be solved by a type cast the type is reinforced to T gt S by applying the dummy function tomap with the following definition name tomap parameters x T gt lt S result type T gt S body x The refused body of upd is replaced by x upd tomap lt lt y z gt gt and this is accepted 1999 Deloitte amp Touche Bakkenist ExSpect is a registered trade mark of ASPT 51 Deloitte amp Touche Bakkenist AN ExSpect User Manual Recursive definitions Unlike type definitions function definitions need not be defined before their use This allows
44. erroneous terms but they may occur while evaluating a term involving variables In applications of the cond function the branch that is not chosen is not evaluated which could have aborted otherwise So if a 0 then 0 else b a fi and if a elt dom M then M a else 0 fi are not aborting terms 1 Discuss the correctness of the following function application terms Evaluate the correct ones if not 221 then 6 1 else O lt 0 4 1 gt 1 tail a elt tail b if 627 then 6 0 else 5 1 fi o 1999 Deloitte amp Touche Bakkenist ExSpect is a registered trade mark of ASPT 46 Deloitte amp Touche Bakkenist AN Implicit mapping construction and quantors ExSpect User Manual 0 4 1 5 a head a Gb a b 1 1 1 upd c 1 2 5 41 0 99 6 4 pit lt lt 8 4 1 0 gt gt 2 Do the following boolean terms always evaluate to true If not give a counterexample The variables a b have type num s has type str and A has type num head s cat tail s s not a elt A or a union A 2 A not a elt b a 2 a 2 a and a 1 a 1 We have constructed mappings by explicit enumeration Mappings can also be implicitly constructed The syntax is x A Ey Here x must be an identifier A a term of set type 1 e containing sets or mappings and Ex a term that may contain x as parameter If A is of type B the parameter x is understood to have type B Also mappings have a set type since they contai
45. es of these processors will be search add remove and change Click with the left mouse button on the Processor button a 2 Click with the left mouse button in the System Definition window at the place you want to put the processor Now a processor with an automatically generated name will appear 3 We repeat and 2 until we have four processors in the System Definition window o 1999 Deloitte amp Touche Bakkenist ExSpect is a registered trade mark of ASPT 10 Deloitte amp Touche Bakkenist AN Connecting places stores and processors ExSpect User Manual 4 By double clicking a processor the Processor Definition window will open In the Name box of this window we can give each processor it s appropriate name use the names search add remove and change Before we can finish the processor definitions we have to place the connections between our objects The following connections have to be made The store contents_phone_book has to be connected to all processors A connection from the channel entry_to_add to the processor add A connection from the channel number_to_search to the processor search A connection from the processor search to the channel answer A connection from the channel entry_to_remove to the processor remove A connection from the channel entry_to_change to the processor change Click with the left mouse button on the Connector button cy po 2 dq SS Select the source of you
46. es tokens for its output channels The production of tokens may be subject to a delay Delayed tokens become available only when the simulation clock has advanced the same amount of time Under which conditions a processor becomes activated and which tokens it may consume and produce is defined by the specification of the processor How a processor is specified is defined in the next subsection Systems A certain set of processors and channels can be grouped together in a subnet or system Such a system can be used to build larger systems by connecting some special channels or pins within the subsystem to the channels of the larger system Connecting a processor or subnet into a larger net 1s called installing The final model is a system without pins This way of hierarchical modelling corresponds to the well known and intuitively clear DFD data flow diagram modelling technique In standard Petri net theory processors are called transitions and channels are called places 1999 Deloitte amp Touche Bakkenist ExSpect is a registered trade mark of ASPT 55 Deloitte amp Touche Bakkenist AN ExSpect User Manual Processor definition We now can explain how processors are defined and installed Like a function a processor has a name parameters and a body It also has a precondition The parameters are divided into input pin output pin store pin value and function parameters The parameters consist of a name and a type fo
47. from a mapping the set of points where the maximum is reached So for example dommax x 1 2 3 x x 4 1 3 3 Define a function torel of signature T gt S gt T gt lt S that converts a set valued mapping to the corresponding relation If lt lt a B gt gt elt f holds and b elt B then also a b elt torel f must hold and vice versa Hint combine the union and rng quantors ExSpect types and sets can mean the same but are used in different context The same holds for functions and mappings A type construction means a certain set of values that may be infinite A set is a term that has a type a set type usually starting with a symbol and is always finite When a type is needed a set 1s not accepted and vice versa A function has a signature and means a set of pairs that may be infinite A function is always implicitly given by its parameters and a defining term A mapping has a type with a gt symbol in it and 1s always finite It may be explicitly or implicitly given In the last case a parameter a set term and a defining term must be given The following expressions are incorrect terms for this reason What is meant by the last non term can be correctly formulated by the stretch function giving the integers in a certain range o 1999 Deloitte amp Touche Bakkenist ExSpect is a registered trade mark of ASPT 53 Deloitte amp Touche Bakkenist A ExSpect User Manual expres
48. hort rehearsal here In the simplest form a processor copies the value from an input channel to an output channel without change This is expressed in the processor s body with an assign statement output lt input This means that the value of the token produced for the channel output is the same as the value of the token on channel input We also saw that we could specify a delay by which the output token should be available This is expressed by output lt input delay 2 0 1999 Deloitte amp Touche Bakkenist ExSpect is a registered trade mark of ASPT Sul Deloitte amp Touche Bakkenist AN ExSpect User Manual which means that the token for channel output becomes available only 2 0 time units after the moment of firing of the processor We saw furthermore that a processor could select output channels under certain restrictions This is expressed by an if statement if input gt O then output input fi This means that a new token value for channel output will only be produced if the token value of channel input 1s positive The statement if input O then output lt input else output2 input fi expresses that negative values and are copied to output and positive values are copied to output2 It is even possible to impose restrictions on the input token before taking it into an input channel By means of preconditions it is possible to select token
49. ic truth is a registered trade mark of ASPT 75 Deloitte amp Touche Bakkenist AN 5 2 Numerical functions ExSpect User Manual This section shows all functions with numericals integers as a result type or as an argument in the modules basic and utils abs x num num add x num y num num add x num y num num add n num x real real add x real n num real add x num y num num botint x num num denominator x num num div x num y num num even n num bool frc x num num ecd x num y num num ge x num y num bool et x xnum y num bool isint x num bool le x num y num bool It x xnum y num bool max x num num max x num y num num max x T num num max x num num min x num num min x num y num num min x T gt num num 1999 Deloitte amp Touche Bakkenist ExSpect utils x absolute value basic x y utils z ylz x utils real n x utils x n utils y added to each element of x utils floor of x largest integer less than equal to x basic the denominator of a rational number basic x div y truncated utils 1s n even utils fractional part of x basic x y greatest common divisor utils x gt y utils x gt y utils is x an integer utils x lt y utils x y utils z ze x and forall y x z gt y maximum of set x utils x max y utils max rng x
50. ion with minimum I maximum u and expectation e basic first element of x utils yly e T and exists ze S y gt lt z e x basic second element of x utils z ze S and exists y e Tj y gt lt z e x basic arbitrary though deterministic element from X stat a random number poisson basic x gt 0 utils x gt 0 utils x y utils x y basic lt lt x y gt gt pair of x and y stat a random number between 0 and 1 basic x y utils z ylze x basic x y utils z ylze x utils real n x is a registered trade mark of ASPT 72 Deloitte amp Touche Bakkenist AN rdiv x real n num real rdiv x num y num num rdiv x real y real real real x num real real x str real rest x ST ST restrict x T gt S y ST T gt S rev x str str reverse x T T rint a real b real seed real real rng x T 5S S scan x str y str bool scanrest x str y str str sdiff x T y T T set x T gt bool ST set x T T sin x real real size x T num size x T num sqrt x real real stobag x T T gt num str x num str str x real str strncmp x str y str n num bool stretch x num y num num stretch x num y num num strlen x str num student n real seed real real sub x num y num num sub x num y num num 1999 Deloitte amp Touche Bakkenist ExSpect ExSpect
51. l real reverse x T T set x T T size x T num stretch x num y num num sub x num y num num sub x real y real real sum x num num sum x real real tail x T T 1999 Deloitte amp Touche Bakkenist ExSpect ExSpect User Manual utils x with each member incremented by y utils x with each member incremented by y basic the concatenation of x and y utils x occurs in y utils x with the last member removed basic the first member of x basic y with x added as head utils the last member of x basic a list containing all members of x utils the maximum in x utils the maximum in x utils the minimum in x utils the minimum in x utils x with each member replaced by its value module y utils each member of x multiplied by y utils each member of x multiplied by y utils each member of x divided by y utils each member of x divided by y utils list x in reverse order basic the set of members of x utils number of members of x utils list containing all members of z x lt z lt yj utils each member of x subtracted by y utils each member of x subtracted by y utils the sum of all numbers in x utils the sum of all numbers in x basic the tail of x is a registered trade mark of ASPT 84 Deloitte amp Touche Bakkenist AN 5 10 Mapping functions This section shows all mapping functions all x T gt bool
52. lace you want to put the store Now a store with an automatically generated name will appear By double clicking a store with the left mouse button the Store Definition window will appear In the Name box of this window we can give the store its appropriate name The name we use for our store is contents_phone_book Press the OK button to save and close the Store Definition window The contents of the resulting system definition window will be something like Figure 2 1999 Deloitte amp Touche Bakkenist ExSpect is a registered trade mark of ASPT 8 Deloitte amp Touche Bakkenist A ExSpect User Manual entry_to_add number to search contents phone book entry to remove answer entry to change Figure 2 Defining and In the next phase we have to think about the types that need to assigning types be assigned to the channels and stores Through the channel number to search a name can be entered so the type of this channel must be str string The assigning 1s done in the following way 1 Double click with the left mouse button the channel number to search The Channel Definition window will open 2 Enter str in the Type box 3 Press OK to save and close the Channel Definition window The channel answer produces the searched phone number or if no such name exists in the phone book Not found so the type we assign to answer is also str By using the channel entry to add we can add a new entry name and phone n
53. le for example pump ex 8 Choose OK In the System Definitions window double click the system main to view the system petrol service station and its environment see Figure 4 car arrived car refueled Lu generate arrivals UM measue throughput time I car drives on count cars driven on Figure 4 System main All interaction of the service station with its environment is the arrival or departure of cars The environment is built with building blocks from a library The system labelled generate arrivals 1s an installation of the building block generator This system generates tokens of type Car and places them in the channel car arrived This models the arrival of cars at the o 1999 Deloitte amp Touche Bakkenist ExSpect is a registered trade mark of ASPT 19 Deloitte amp Touche Bakkenist AN Adding channels ExSpect User Manual service station The system petrol_service_station consumes the cars from the channel car_arrived and depending on the situation puts them in the channel car_refueled or car_drives_on The systems measure_throughput_time and count cars driven on collect all kinds of simulation information Double click the system petrol service station This 1s the system that has to be completed It has one input connector car arrived and two output connectors car drives on and car refueled Figure 5 shows the subsystem we are going to build r3 rome of pump _ 2 e O
54. lement of x incremented by y basic floor of x largest integer lt x basic x basic e x utils fractional part of x utils x gt y utils x gt y utils x lt y basic x utils x y utils z ze x and forall y x z gt y maximum of set x utils x max y utils max rng x utils the maximum of x utils x utils z z x and forall y x z lt y minimum of set x utils x min y is a registered trade mark of ASPT 78 Deloitte amp Touche Bakkenist AN min x T gt real real min x real real mult x real y real real mult x real y real real mult n num x real real mult x real n num real mult x real y real real num x real num pos x real bool pow x real y real real rdiv x real y real real rdiv x real y real real rdiv n num x real real rdiv x real n num real rdiv x real y real real real x num real real x str real sin x real real sqrt x real real str x real str sub x real y real real sub x real y real real sub n num x real real sub x real n num real sub x real y real real sum x real real sum x T gt real real sum x real real 1999 Deloitte amp Touche Bakkenist ExSpect User Manual utils min rng x utils the minimum of x basic x y utils z ylzex utils real n x utils n x utils each element of
55. les can be answered negative Figure 7 Simulation results Other scenarios As explained in the case description the management want to know what the best investment is to reduce the number of cars that drive on If possible they also want to reduce the average throughput time For each investment scenario you can change the model and run a simulation When you have done that and carefully analysed the results you can advise the management of the service station 1999 Deloitte amp Touche Bakkenist ExSpect is a registered trade mark of ASPT 30 Deloitte amp Touche Bakkenist AN ExSpect User Manual J The language Introduction Materials Learning to specify in a functional language is like learning a skill you have to know about the materials you are working with about the tools to work with and about how to operate the tool on the materials in order to create a result In a functional specification the materials we use are types and values The tools we use are type and value constructions and expressions The result we want to obtain is a token value In ExSpect this will be a specification of part of the body of a processor in this case a specification of how to build an output token value from the input token values In the tutorials in the previous chapters we already saw that the body of a processor specifies the exact way to produce output token values from input token values We will give a s
56. like in a processor definition can be specified Systems can be polymorphic like processors Pins can be drawn in the graphical editor value and function parameters must be added after opening the signature window For systems even processor and sub system parameters are possible This advanced feature is seldom used and outside the scope of this tutorial Furthermore channels and stores are defined and processors and subsystems installed Defining channels and stores 1s done by drawing them and then giving a name and type construction and for channels optionally an initialisation A store initialisation is a term of the store type It may contain variables from the value and function parameters A channel initialisation may contain one or more terms of the channel type It may also be absent When installing subsystems their parameters must be bound like for processors o 1999 Deloitte amp Touche Bakkenist ExSpect is a registered trade mark of ASPT 59 Deloitte amp Touche Bakkenist AN Exercises Modules and scoping Exporting definitions Local definitions ExSpect User Manual 1 Convert the system FINANCE to a system with 2 different processors one for addition and the other for subtraction 2 Define a polymorphic processor with an input and output pin of type T and a store pin of type bool Whenever the store has value true the input is copied to the output with a delay of time unit When the sto
57. lz ex utils z ylz ex basic x pick x basic x Vy basic sum y x 1 number of elements of x utils z ylzex utils z ylze x utils x lt y utils sum y x y utils sum y x y utils Union_ y x y union of all elements of x basic x union y In these functions seed should be in the open interval 0 1 1 e 0 lt seed 1 It can be obtained by using random 1999 Deloitte amp Touche Bakkenist is a registered trade mark of ASPT 82 Deloitte amp Touche Bakkenist AN bernouilli p real seed real real binomial n real p real seed real real chisq n real seed real real erlang m real k real seed real real nexp m real seed real real gamma lI real k real seed real normal m real v real seed real real PERT beta l real u real e real seed real poisson m real seed real real random seed real real rint a real b real seed real real student n real seed real real uniform a real b real seed real real 5 9 List functions ExSpect User Manual stat draw from a bernouilli distribution with expectation p 0 lt p lt 1 stat draw from a binomial distribution with expectation p n 0 lt p lt 1I and n should be a non negative integer stat draw from a X 2 distribution with n degrees of freedom n should be a non negative integer stat draw from an erlang distribution with expec
58. n animation dashboard object 4 Click the left mouse button at the place you want to put the animation object 5 Double click the new animation object A Dashboard Objects Properties window appears In the Label box type Traffic light 7 In the Place box type main petrol_service_station number_of_cars_in_queue In the first row of the Animation Frames list type green bmp In the second row of the Animation Frames list type green bmp 10 In the third row of the Animation Frames list type green bmp 11 In the fourth row of the Animation Frames list type red bmp 12 Size the animation object to make it look like a traffic light 13 Choose OK It is also possible to view the number of tokens in a channel 1 Double click the channel queue A property window appears 2 Check the checkbox Counter Visible 3 Choose OK Resume the simulation by pressing the Play button Now you will see that the traffic light turns red when the queue contains three cars Close the System Animation windows and wait until the simulation is finished the simulation will run faster if all windows are closed 1999 Deloitte amp Touche Bakkenist ExSpect is a registered trade mark of ASPT 27 Deloitte amp Touche Bakkenist AN Simulation results ExSpect User Manual The systems measure_throughput_time and count_cars_driven_on collect all kinds of simulation information For this case the number of cars th
59. n has a single signature containing only types without type variables In the following table we give a selection of simple functions with their signatures 1999 Deloitte amp Touche Bakkenist ExSpect is a registered trade mark of ASPT 41 Deloitte amp ExSpect User Manual signature boolbool bool bool bool bool bool bool str str str strstr strstr example not true false and true false or true Oh cat boy head Gee tail Gee false false true Oh boy G ee The fourth line in this table defines the simple function cat with two string parameters and a string result From the example can be deduced that the function can be used in infix mode 1 e the function name or symbol between the parameter terms Its effect is to concatenate its two parameter strings In chapter 5 is the exact nature of these functions is explained Every function with two parameters can be used in infix mode However in nested function applications like a and b or c one is advised to use brackets for priority Touche Bakkenist AN name not and or cat head tail Overloading The same function symbol and name is sometimes used for several simple functions An example is formed by the arithmetical functions The arithmetical manipulation of reals and nums is different Yet when specifying an addition one wants to use the symbol irrespective of the kind of number
60. n sets of pairs B may even contain type variables when it occurs in a term with variables The result type is B gt C where C is the type of Ex The explicit value is obtained by constructing the set of pairs lt lt a 1999 Deloitte amp Touche Bakkenist ExSpect is a registered trade mark of ASPT 47 Deloitte amp Touche Bakkenist AN ExSpect User Manual b gt gt where a subsequently takes all values from A and b is obtained by replacing x by a Some examples of this construction are given below mapping type explicit value y a b d ltail y str gt str lt lt a gt gt lt lt b gt gt lt lt d gt gt x 1 3 H a x 1 num a num lt lt 1 a 0 gt gt 3 a 2 gt gt z 01 HO eltz Snum bool lt lt false gt gt lt lt 0 true gt gt The implicit mapping construction can be combined with the rng function to construct sets in an implicit way The term rng x A Ex is equivalent to the mathematical notation for sets The above examples combined with rng give the following results term type value rng y a b d Htail y str rng x 1 2 3 l a x 1 a num a 0 a 1 a 2 rng z 0 l0 elt z num bool false true There are other functions quantors that combine well with implicit mappings We give a table name signature example all T gt bool bool all x 1 2 3 Ix gt O true any T gt bool bool any x 1
61. n with ExSpect the user 1s referred to Aal94a Aal94b Aal96a Aal96b DE95 Hee94 Ros90 and JR91 AAKea96 W M P van der Aalst A Aarts H Koppelman and R V Schuwer et al Informatiesystemen Modelleren en Specificeren Open Universiteit Heerlen 1996 1n Dutch Aal94a W M P van der Aalst Procesmodelleren met behulp van Petri netten Informatie 36 4 244 252 1994 in Dutch Aal94b W M P van der Aalst Putting Petri nets to work in industry Computers in Industry 25 1 45 54 1994 Aal96a W M P van der Aalst Petri net based Workflow Management Software In A Sheth editor Proceedings of the NFS Workshop on Workflow and Process Automation in Information Systems pages 114 118 Athens Georgia May 1996 Aal96b W M P van der Aalst Three Good reasons for Using a Petri net based Workflow Management System In S Navathe and T Wakayama editors Proceedings of the International Working Conference on Information and Process Integration in Enterprises IPIC 96 pages 179 201 Camebridge Massachusetts Nov 1996 1999 Deloitte amp Touche Bakkenist ExSpect is a registered trade mark of ASPT 88 Deloitte amp Touche Bakkenist AN AH97 DE95 Hee94 Jen92 JR91 Pal97 Pet8 1 Rei85 Ros90 SL96 ExSpect User Manual W M P van der Aalst and K M van Hee Workflow Management Modellen Methoden en Systemen in Dutch Academic Service
62. new number say 040 2471234 Select the channel entry to change 2 Press the right mouse button and select Add Token from the pop up menu 3 Enter Gary in the Name field and 040 2471234 in the Number field Press the Play button We see that contents phone book is updated 5 Check the value of contents phone book by looking at the dashboard table Now we want to remove an entry from our phone book So suppose Mary marries Gary and moves in with him Now we can remove Mary from our phone book Select the channel entry to remove 2 Press the right mouse button and select Add token from the pop up menu 3 Enter Mary in the Add Token window Press the Play button We see that contents phone book is updated 5 Check the value of contents phone book by looking at the dashboard table object o 1999 Deloitte amp Touche Bakkenist ExSpect is a registered trade mark of ASPT 16 Deloitte amp Touche Bakkenist AN Searching numbers in the phone book ExSpect User Manual Finally we want to search for a phone number Since it has been a long time since we spoke Jack we are going to search for his phone number Select the place number_to_search 2 Press the right mouse button and select Add Token from the pop up menu 3 Enter Jack in the Add Token window 4 Press the Play button Now we see that a number is searched in the phone book and an anwer is produced in the channel answer To check the contents of
63. ng the following steps 1 In the submenu Add of the Object menu select Store or use the store button Eh 2 Move the mouse pointer over the gas station system window The cursor will change into the symbol for a store Click the left mouse button at the place you want to put the store Double click the new store A property window appears In the Name box type number_of_cars_in_queue In the Type box select the type num Choose OK oe i eS Now that all channels and stores are created it 1s time to create the processors They have already been discussed in the previous paragraph 1 Inthe submenu Add of the menu Object select Processor or use the processor button vl 2 Move the mouse pointer over the gas station system window The cursor will change into the symbol for a processor 3 Click the left mouse button at the place you want to put the processor 4 Double click the new processor The Processor Definitions window appears o 1999 Deloitte amp Touche Bakkenist ExSpect is a registered trade mark of ASPT 22 Deloitte amp Touche Bakkenist AN Adding connections ExSpect User Manual 5 In the Name box type decide 6 Choose OK Repeat this for the processors start service and end service Before we can finish the definition of the processors the channels stores pins and the processors have to be connected Connecting channels stores pins and processors 1s straightforward To connect the
64. oken combination is if statements selected the if predicate determines what to do with the tokens once they are selected So a processor without precondition 1 e true as precondition and body if P then S fi differs from the processor with precondition P and body S The first 1s activated by any input token combination if this combination does not satisfy S it is consumed without causing any output or store update The second does not consume token combinations that do not satisfy S so they may be left for another round or for other processors For token combinations that do satisfy S both act the same 1999 Deloitte amp Touche Bakkenist ExSpect is a registered trade mark of ASPT 58 Deloitte amp Touche Bakkenist AN Polymorphy Systems ExSpect User Manual Like functions processors can be polymorphic 1 e their signature types may contain type variables When a polymorphic processor is installed the installed types must match the definition types More explicitly the same type variable T must correspond to the same installed type Consider the following polymorphic processor copy input inpt T output outpt T val t real body outpt inpt delay t This processor cannot be installed by connecting the input pin to a channel of type num and the output pin to a str channel Nor can it be installed by producing for example a num term for the value parameter t When defining systems parameters
65. ool ExSpect These cases are used to show the use of ExSpect for creating executable specifications of high level Petri nets It is recommended to use the on line help for further explanation on the user interface The first tutorial illustrates the creation of a small telephone number database The resulting specification is directly executable This first tutorial gets the user acquainted with the use of the tool The second tutorial uses predefined building blocks to demonstrate the power of simulation The tool tutorials are followed by a language tutorial Chapter 3 All features of the ExSpect language are discussed and illustrated with useful examples Chapter 4 contains a formal description of the syntax of the ExSpect language Chapter 5 1s a reference manual containing all library functions The last chapter is the bibliography It contains numerous useful references to related material 1999 Deloitte amp Touche Bakkenist ExSpect is a registered trade mark of ASPT Deloitte amp Touche Bakkenist AN 1 Tutorial 1 Introduction Description of the case ExSpect User Manual Building a phone book This tutorial will give an introduction to the way a specification of a simple information system is built The purpose of this tutorial is to show the reader what considerations and steps are taken when building an actual system The information system we are going to discuss is a phone book A phone
66. ort type id z from type fundef id par I z expr type procdef proc id lt afpar gt P preprio P z lt stat gt sysdef sys id lt afpar gt P obj preprio pre expr prio expr pre expr prio expr prio expr pre expr stat id lt expr delay expr bounds real real P expr then lt stat gt 1999 Deloitte amp Touche Bakkenist ExSpect is a registered trade mark of ASPT 64 Deloitte amp Touche Bakkenist AN obj actarg valarg avarg expr type ExSpect User Manual elif expr then stat gt else lt stat gt p skip channel store id type in id form string init expr id 2 id lt avarg gt Y in out store inhibit fun lt id gt val lt expr gt actarg valarg id const expr y id id expr I expr T 1d Y expr gt T expr id id arg Y if expr then expr elif expr then expr else expr fr lt lt lt expr gt gt gt lt expr gt lt l lt expr gt l expr id z 7 1 gt 4 p 09 gt lt pet lt
67. pe constructors Irregular functions are functions that have no finitely representable signature The set list and record constructors are irregular functions They can be used with terms as in the following examples 1999 Deloitte amp Touche Bakkenist ExSpect is a registered trade mark of ASPT 44 Deloitte amp Touche Bakkenist AN ExSpect User Manual 1 1 3 1 5 2 2 2 5 lt l1 1 3 1 5l I2 2 5l name J cat Doe sal 10 10 30 name J Doe sal 3000 The pair constructor prod is not irregular It has signature T S gt T gt lt S Like the set and record constructors 1t can be used with terms as in the following example It has been included here because of its similarity with the previous two functions 1 1 1 2 5 7 gt gt 1 21 7 9 gt gt Also the record projection symbol and update upd functions are irregular The following examples illustrate their use a 5 b q Qa 5 a 5 b q upd b r c true a 5 b r c true These functions are called irregular because their signature cannot be represented finitely although the allowed parameter types and the way they affect the result type are completely determined The set constructor accepts one or more parameters of type T and yields a result of type T The record constructors H lo accept terms of types Tj To and yield a term of type l T4 lo To The list constructor
68. pe constructors are applied Their values are represented by constructions containing constants and special function symbols called construction symbols We first treat basic types and their values then type constructors and constructed values We conclude by treating type definitions Basic types and The basic types are bool str num real and void constants bool The type bool contains two values the boolean constants false and true Str The type str contains all printable ASCII strings These strings are represented between quotes So AC DC is a constant of type str To represent a quote in a string constant it must be doubled So a represents the string a The empty string is which is also a valid constant ASCII strings containing non printable characters for example new lines are not in this type Num The type num contains the rational numbers 1 e natural numbers 0 1 2 negative integers 1 2 and their quotients like 5 17 or 191 27 The rational numbers have no upper or lower bound ExSpect can handle 1000 digit numbers and their quotients Of course manipulations with large numbers will be rather time consuming Real The type real is a numeric type like num To distinguish them from nums reals must have a single decimal dot somewhere Note that for example 2 and 2 are different constants although they might mean the same to a user o 1999 Deloitte amp Touche Bakkenist ExSpect is a registered
69. phone book Second phone numbers that are added are not already in the phone book Finally when a search for a phone number is performed the entered name is uniquely present in the phone book A more realistic system won t be based on these assumptions and will have to act accordingly in these kinds of events Before we start with the actual building of a system some general actions have to be taken Start ExSpect Next a new file has to be defined for the specification Selecting New from the File menu does this By selecting Save As from the File menu we can give our file an unique name we have chosen the name phone 1999 Deloitte amp Touche Bakkenist ExSpect is a registered trade mark of ASPT 6 Deloitte amp Touche Bakkenist AN Building the system Placing channels ExSpect User Manual 4 Every specification needs at least one system so we have to define a system for our phone book To do this we select System Definitions from the Components menu Now a window opens with all defined systems this window is empty in our case for the simple reason that we have not yet defined a system Now we click with the left mouse button on the New button a window opens in which we can give a name to our system the default name is System we choose the name Phone book has to be one word After clicking the OK button with the left mouse button the System Definition window of the Phone book system will op
70. pin car arrived with the processor decide do the following Click on the Connector button amp Click on the source of the connection In this case this 1s the input pin car arrived Click on the destination of the connection In this case this 1s the processor decide Repeat this for the following connections The store numbers of cars in queue is connected to the processors decide and start service A connection from the processor decide to the channel queue A connection from the processor decide to the output pin car drives on A connection from the channel queue to the processor start service A connection from the processor start service to the channel being served A connection from the channel being served to the processor end service A connection from the processor end service to the output pin car refueled A connection from the processor end service to the channel pump free A connection from the processor pump free to start service o 1999 Deloitte amp Touche Bakkenist ExSpect is a registered trade mark of ASPT 23 Deloitte amp Touche Bakkenist AN Defining processors ExSpect User Manual The last step in the creation of the service station 1s the definition of the processors Remember that the processor decide had to move the car from car_arrived to queue when there was enough room in the queue otherwise it had to be moved to the channel drive_on Also remember that in the first case th
71. plete we have to specify the appropriate type Make the following changes 1 Double click the channel queue A property window appears 2 In the Type box select the type Car 3 Choose OK Repeat this for the channel being served Tip when you place a channel you can use the right mousebutton A pop up menu appears from which you can select the channel type The channels being served and pump free model the situation that a car is being served or not In the initial state there 1s one token in the channel pump free The type of this channel is not important The fact that the pump is free is denoted by the fact that the channel contains a token The type of that token 1s not relevant To keep the specification simple we choose the type str o 1999 Deloitte amp Touche Bakkenist ExSpect is a registered trade mark of ASPT 21 Deloitte amp Touche Bakkenist AN Adding a store Adding processors ExSpect User Manual Double click the channel pump_free A property window appears In the Type box select the type str In the Initial Tokens list type pump in the first row Choose OK oe BR The processor decide needs to know the number of cars in the queue This number is kept in the store number of cars in queue When a car is put in the queue the value of this store 1s increased by one When a car 1s removed from the queue the value is decreased by one Add the store to the specification by performi
72. r connection for example number to search Moving the mouse pointer above the object and pressing the left mouse button does selecting 9 Select the destination of your connection for example search 10 Repeat 1 2 and 3 until all connections are made Note By double clicking the connector button several connections can be made without having to select the connector button again The same can be done when placing channels stores systems and processors Pressing the pointer tool button does deselecting a button B The contents of the resulting System Definition window is shown in Figure 3 1999 Deloitte amp Touche Bakkenist ExSpect is a registered trade mark of ASPT 11 Deloitte amp Touche Bakkenist AN ExSpect User Manual entry_to_add add number to search contents phone book Q9 entry to remove search remove change answer entry to change Figure 3 Should one of the connections accidentally have been placed wrong then the connection has to be removed and the processor definition updated The following can be done to correct such an error 1 Double click the wrongly connected processor the Processor Definition window will open 2 Select the wrong connection in the Connections box by pressing the button in front of the connection in question 3 Select Delete from the Edit menu 4 Press OK to save and close the Processor Definition window The next step 1
73. r function parameters a signature The precondition contains a predicate a term of type bool The body consists of a statement list A statement is a conditional statement the skip statement or an assignment Commas separate the statements instead of semicolons indicating that they can be executed concurrently their order has no significance A conditional statement consists of an if predicate a then part and an optional else part The then and else parts are statement lists An assignment consists of an output channel or store name the assignment symbol lt and a term of the same type as the assigned channel or store It may be followed by a delay term of type real preceded by the keyword delay The terms and predicates may contain all variables amongst the parameters except the output channel parameters Processor installation Processors are installed in systems Upon installing pins are linked to channels and pins of the system terms are attached to value parameters and functions to function parameters Their types must match of course Terms attached to a value parameter may only contain value parameter names of the system as variables these must be filled in when the system itself 1s installed in a higher order system The topmost system has no value or function parameters nor pins Value and function parameters are static their values definitions are bound to the variables when they are installed In the topmost system
74. re has value false the input tokens are left untouched This processor can be used to model a transistor or a lazy bureaucrat 3 Define a subsystem with input pin of type T and output pin of type T If the set A arrives as input the output must consist of all the individual elements of A ExSpect has a number of libraries containing general purpose types functions processors and systems It 1s possible to add one s own libraries A library is called a module in the language modules can be imported by including them The order in which modules are included is important When creating a module definitions that are to be used outside the module must be exported Types can be exported with or without their defining type construction In the last case all possible access functions of the type must be defined in the module i e the type is abstract In this case it is possible to implement the type and its access functions differently without the users of the type noticing it In the other case this 1s impossible Also definitions that are accessible by users must be exported Modules are one way of limiting the scope of definitions Another way is by local definitions that may accompany a single definition The local definitions are not known outside the definition that they accompany Local definitions may be used for creating more efficient definitions when recursion 1s involved 1999 Deloitte amp Touche Bakkenist Ex
75. real max x num num max x real real minus x num num minus x real real min x num num min x num y num num min x T gt num num min x Sreal real min x real y real real min x T gt real real min x num num min x real real mod x num y num num mod x num y num num mod x num y num num mult x num y num num mult x num y num num mult x real y real real mult x real y real real mult n num x real real mult x real n num real mult x num y num num mult x real y real real ne x T y T bool nexp m real seed real real normal m real v real seed real real not x bool bool 1999 Deloitte amp Touche Bakkenist ExSpect User Manual utils max rng x utils the maximum in x utils the maximum in x utils x utils x utils z z x and forall y x z lt y minimum of set x utils x min y utils min rng x utils z z x and forall y x z lt y minimum of set x utils x min y utils min rng x utils the minimum in x utils the minimum in x basic x mod y utils zmodylze x utils x with each member replaced by its value module y basic x y utils z ylzex basic x y utils z ylzex utils real n x utils n x utils each member of x multiplied by y utils each member of x multiplied by y utils x y x not equal to y st
76. s added This is done by overloading attaching more signatures to the same function name as shown in the table below 1999 Deloitte amp Touche Bakkenist ExSpect is a registered trade mark of ASPT 42 Deloitte amp Touche Bakkenist AN Polymorphy ExSpect User Manual name signature examples add num numnum 4 5 2 3 22 15 real real real 0 8 0 67 1 47 num num num 4 5 0 2 3 4 5 22 15 sub num numnum 4 5 2 3 2 15 real real real 0 8 0 67 0 13 mult num numnum 4 5 x 2 3 8 15 real real real 0 8 x 0 67 0 536 rdiv num numnum 4 5 2 3 6 5 real real real 0 8 0 67 1 194 gt num num bool 527 2 false gt real realbool 5 5 7 false Note that the name of the above functions differ from the symbol used Also note the third definition of addition that manipulates sets of numerals A more extensive list of numeric functions can be found in the appendix The priority in nested arithmetical terms like a b c is the normal arithmetical priority Note the extra brackets that are needed in the term 4 5 2 3 We encountered the division symbol earlier in the values belonging to type num Polymorphy can be seen as infinite overloading For instance set union does not regard the type of the contained elements However the union of sets of different type 1s illegal the result cannot be typed The signatures of the union thus contain num num num str stro str but not
77. s from an input channel pre input gt 0 A processor with these preconditions only accepts tokens on channel input which are positive All other tokens on that channel will not trigger the processor 1999 Deloitte amp Touche Bakkenist ExSpect is a registered trade mark of ASPT 32 Deloitte amp Touche Bakkenist AN ExSpect User Manual The value of the output token can be derived from the value of input tokens by means of a function output lt function input where function a J In this tutorial we will learn how to specify the body of a function that 1s how we can derive a new value from other values First of all we will learn how to use types in order to classify values This consists of an introduction of basic types and type constructors Together with types we will introduce constant values of these types Together with type constructors we will show how to construct new values with value constructors Types and values will be the materials we are going to use Type constructors and value constructors will be the first tools we will handle Next we will see how to define and use functions another set of tools The ExSpect language and tool can be used in two ways One way is to combine predefined building blocks processors and subsystems to specify a large system However not all systems can be built in this way It may be necessary to adapt building blocks or even
78. s to give the processors the required functionality so they will have the appropriate input output behaviour In the remainder the functionality of each processor is given and described This functionality is entered in the definition box of the Processor Definition window The inexperienced reader probably will not understand the full functionality that o 1999 Deloitte amp Touche Bakkenist ExSpect is a registered trade mark of ASPT 12 Deloitte amp Touche Bakkenist AN Processor search Processor add ExSpect User Manual is entered This is no problem since the purpose of this tutorial is to give the reader an idea on how to work with ExSpect The language that is used to specify the behaviour is explained in detail in chapter 3 The way we want the processor search to behave is the following if the entered query is in the phone book then return the phone number else return a message that the number was not found This is implemented in the following way 1 Double click the processor search 2 Enter the following text in the definition box of the processor definition window if number to search elt rng x contents_phone_book x name then answer lt pick set x contents_phone_book x name number to search ephone number else answer not found 3 Press OK to save and close the processor definition window The processor add inserts a new phone number into the phone book This 1s implemente
79. se this feature It 1s not pleasant to hunt for definitions that are too deeply nested It 1s better to put definitions on the top level unless they are specifically linked to one definition We conclude this lesson by treating the scope of variables The smallest and strongest scope is the variable in an implicit mapping term In the term DcAJE any variable x within term E is bound by the mapping and thus is interpreted as an element of the set A An occurrence of x in A is not bound by it so it must occur in some wider scope An example is x stretch 0 x x1 in a function body where x is a parameter Here the x in x41 1s the mapping variable whereas the one in stretch 0 x 1s the function parameter Parameters and local definitions in a definition form the second scope The variables there take priority over those in the third scope the global and imported definition names Define a function freqcount of signature str str2num such that freqcount a b gives the number of times that the string b occurs as substring of a For example freqcount abracradrabra ra 4 Compute how many recursion steps are needed if the length of ais n and of b is m Improve the efficiency of your definition the most efficient definition requires n steps o 1999 Deloitte amp Touche Bakkenist ExSpect is a registered trade mark of ASPT 62 Deloitte amp Touche Bakkenist AN 4 Syntax Release note Reserved words No
80. sion term to use x boollnot x x false true Hnot x all x numlnot x x lt 0 true set x numl5 lt x lt 13 stretch 6 12 The following expressions are incorrect types expression type to use false true bool 5 6 7 num cannot be strengthened set x numl5 x 13 num cannot be strengthened 1999 Deloitte amp Touche Bakkenist ExSpect is a registered trade mark of ASPT 54 Deloitte amp Touche Bakkenist A ExSpect User Manual 3 3 Lesson 3 The dynamic part Introduction The dynamic part of the language is about modelling processes and their interaction The theory behind the dynamic part of ExSpect is Petri net theory We will give a brief introduction into the aspects that are relevant for modelling and specification Petri nets A Petri net is a network of active objects called processors and passive objects called channels The channels may contain any number of tokens Depending on the kind of channels involved the tokens in it may be interpreted as units of information control or even physical objects A special channel called store contains a single token at all times Processors Processors can be connected to channels in three ways for input output and both This is represented graphically by arrowheads If the tokens in the input channels of a processor satisfy certain conditions the processor may become activated It then consumes certain tokens from its input channels and produc
81. str tail x T T that x T gt bool T tomap x T gt lt S T gt S topint x num num tovoid x T void true bool uniform a real b real seed real real union x T ST union x T y T ST upd x T gt S y T z S T 5S upd x y 5 1 Boolean functions ExSpect User Manual basic x y utils z ylze x utils each member of x subtracted by y utils each member of x subtracted by y utils real n x utils x real n adt is bag x contained in y bag subset utils x lt y utils sum y x y utils sum y dom x x y utils sum y e x y utils sum y dom x x y utils the sum of all numbers in x utils the sum of all numbers in x basic string x without first character basic the tail of x utils z z e dom x and x z and forall y dom x and x y y 2z the only element in T that is true utils type casting of set of pairs to mapping utils smallest integer gt x utils x converted to void basic truth stat a random number uniform utils Union_ y x y union of all elements of x basic x union y basic update x with x y z basic update x according to y This section shows all boolean functions of the modules basic and utils 1999 Deloitte amp Touche Bakkenist is a registered trade mark of ASPT 74 Deloitte amp Touche Bakkenist AN all x T gt bool bool and x bool y
82. tation ExSpect User Manual In ExSpect version 6 x the following constructions are not supported anymore by the designer and animator e Bundle types e Processor and system parameters The type checker has however not been changed since version 5 so the type checker still supports these constructions That is why the keyword ctype still needs to be listed as reserved word as bounds channel ctype delay default end export form from fun in include inhibit init module out pre prio proc Skip sys store type val void where with if then else fi elif The syntax 1s described in BNF Beckes Nauer form The following special notations are used X A comma separated list of X s X Anything except an X o 1999 Deloitte amp Touche Bakkenist ExSpect is a registered trade mark of ASPT 63 Deloitte amp Touche Bakkenist ExSpect User Manual module line line export dec in id export def where line line end include string dec typedec fundec procdec sysdec typedec type id z from type fundec id par type procdec proc id lt afpar gt T sysdec sys id lt afpar gt T par id type gt actpar in out store val par funpar fun fundec default id gt afpar actpar funpar def typedef fundef procdef sysdef typedef exp
83. tation k m and variance k m 2 k should be a positive integer and m gt 0 stat draw from a negative exponential distribution with expectation 1 m m gt 0 stat draw from a gamma distribution with mean I k and variance l k 2 stat draw from a normal distribution with expectation m and variance v v gt 0 stat draw from a beta distribution with minimum I maximum u and expectation e stat draw from a distribution of a poisson process with intensity m m should be a non negative integer stat draw from a uniform distribution on the open interval 0 1 stat closed interval a b The values of a and b should be integer and a b stat draw from a t distribution with n degrees of freedom The value of n should be a positive integer stat draw from a uniform distribution on the open interval a b a b This section shows all list functions of the modules basic and utils o 1999 Deloitte amp Touche Bakkenist ExSpect is a registered trade mark of ASPT 83 Deloitte amp Touche Bakkenist AN add x num y num num add x real y real real cat x T y T T elt x T y T bool front x T T head x T T ins x T y T T last x T T list x T T max x num num max x real real min x num num min x real real mod x num y num num mult x num y num num mult x real y real real rdiv x num y num num rdiv x real y rea
84. tered trade mark of ASPT 35 Deloitte amp Touche Bakkenist AN ExSpect User Manual Definition if kind credit then total lt total amount else total lt total amount fi The installations are given in the following table name total add credit total credit subtract In the example the values debit credit the conditions amount gt 0 kind credit and the assigned values total amount total amount all are terms Terms can be either atomic constants a variable or constructed by means of functions or quantors from simpler terms In the example debit credit 0 are atomic terms kind amount and total are variables whereas gt are function symbols representing functions We will discuss quantors later We shall first deal with types and values and then turn to terms and functions We then explain in more detail how processors and systems are defined and installed We conclude by explaining how to create and use modules o 1999 Deloitte amp Touche Bakkenist ExSpect is a registered trade mark of ASPT 36 Deloitte amp Touche Bakkenist AN ExSpect User Manual 3 1 Lesson 1 Types and values Introduction Types represent sets of values Basic types are bool str num and real They contain atomic values called constants Non basic or constructed types contain basic types one or more type constructors plus brackets to define the order in which the ty
85. there 1s one petrol pump available The taxicab company is growing and lately 8 of the refuelling takes place at another service station Management suspects that taxi drivers go directly to other service stations to win time They want to use simulation to find answers to the following questions e Do taxi drivers evade the rule to go to the company s service station first e Taxi drivers complain about waiting times of ten minutes or more Is this true e What is the best investment alternative for the service station Should the waiting area for the queue be enlarged should a faster one replace the pump or should a second pump be added Getting started In this tutorial an incomplete model of the Taxicab Company has to be finished so it can be used to run a simulation What has been omitted from the model is the petrol service station o 1999 Deloitte amp Touche Bakkenist ExSpect is a registered trade mark of ASPT 18 Deloitte amp Touche Bakkenist A The main system ExSpect User Manual Perform the following steps to get a copy of an ExSpect specification of the environment of the petrol service station Start ExSpect Select Open from the File menu In the Folders box select the folder Tutorial Petrol Service Station In the File Name box select the file Template ex Choose OK Select Save As from the File menu o A d 2 e oa In the File Name box type a name for the copy of the fi
86. tore pins are not allowed either As an example we use the finance system defined earlier The processor book has the following definition Connections input amount num store total num Pre amount O Val fun parameters kind val str o 1999 Deloitte amp Touche Bakkenist ExSpect is a registered trade mark of ASPT 57 Deloitte amp Touche Bakkenist AN ExSpect User Manual Definition if kind credit then total lt total amount else total lt total amount fi When it is installed with name cr value parameter kind bound to credit input pin amount bound to channel a containing 3 tokens with value 5 3 and 7 respectively store pin total bound to t containing the value 1000 the following can happen The tokens with values 5 7 both satisfy the precondition so any of them may activate cr Suppose 5 1s selected The body is evaluated because of the value of kind the then part is executed So total is updated with 1000 5 In the new situation a contains tokens with values 3 7 and total contains 995 If the token with value 7 has not disappeared in the meantime it can again activate cr and result in total containing 988 The token with value 3 does not satisfy the precondition it will not be consumed by cr For more activations of cr other processors or the end user must insert positive valued tokens in a Preconditions and Precondition predicates determine whether a t
87. ue definition In the following examples simple functions are defined name pi parameters result type real body 3 14159 name triangle parameters x num result type num body x x 1 2 1999 Deloitte amp Touche Bakkenist ExSpect is a registered trade mark of ASPT 49 Deloitte amp Touche Bakkenist AN Polymorphic functions name parameters result type body name parameters result type body ExSpect User Manual headstogether x str y str sir head x cat head y mult x num y num num rng t x t y The last function in fact 1s an extra overloading of the mult function that we saw earlier The choice of the name mult means that we can use the infix symbol for instance in the term 5 4 3 7 meaning mult 5 4 3 7 and yielding 35 28 21 Polymorphic functions are defined by using type variables like in the following examples the set intersection and delete functions followed by mapping update name isect parameters x T y T result type T body rng t x t elt y name del parameters x T y T result type T body set t y not t x name upd parameters x T gt S y T gt S result type T gt S body t dom x union dom y if t elt dom y then y t else x t fi 1999 Deloitte amp Touche Bakkenist ExSpect is a registered trade mark of ASPT 50 Deloitte amp Touche Bakkenist AN Type casting ExSpect Us
88. ull num void lreverse x num gt T num gt T Isnoc x num gt T y T num gt T It x xnum y num bool It x real y real bool Itail x num gt T num gt T Itobag x num gt T T gt num match x str y str bool max x num num max x num y num num max x T num num max x real real max x real y real real 1999 Deloitte amp Touche Bakkenist ExSpect User Manual utils z z dom x and x z y inverse basic x intersect y intersection utils is x an integer utils is x an integer basic is x a num basic 1s x a real utils the last member of x adt concatenation of lists x and y adt append y in front of list x utils x lt y utils x lt y adt 1s x an empty list adt list x without the last member adt first member of list x basic a list containing all members of x adt last member of list x basic x natural logarithm adt the empty list adt reverse of list x adt append y at the back of list x utils x y utils x y adt list x without the first member adt list x converted to a bag utils 1s x head of y utils z z e x and forall y x z gt y maximum of set x utils x max y utils max rng x utils z ze x and forall y x z gt y maximum of set x utils x max y is a registered trade mark of ASPT 70 Deloitte amp Touche Bakkenist AN max x T gt real
89. umber to the phonebook Therefore we define a type entry as the tuple type name str phone number str 1999 Deloitte amp Touche Bakkenist ExSpect is a registered trade mark of ASPT 9 Deloitte amp Touche Bakkenist A ExSpect User Manual 1 Select type definitions from the components menu Now the Type Definitions window will open 2 Add anew type definition by pressing New in the Type Definitions window 3 Enter entry in the name box of the Type Definition window 4 In the definition box the type can be specified in our case name str phone_number str 5 Press OK to save and close the Type Definition window Press CLOSE to close the Type Definitions window Assign entry to entry_to_add The channel entry_to_remove can be used to enter a name to remove a name and the entry belonging to this name Therefore we assign str to the channel entry_to_remove The channel entry_to_change is used to change existing phone numbers so we assign the type entry to entry_to_change This leaves the type of the store contents_phone_book This is a set of entries so the store contents_phone_book has the type entry Placing processors After assigning types to all the channels and stores we have to define the active components of the specification processors In our case we need not define any subsystems because of the simplicity of the system to be designed So we add four processors one for each action that can be taken The nam
90. ve the same elements but are nevertheless different one is a type the other a value The type A contains finite lists sequences of values from A The value constructors for lists is These lists are represented by enclosing its elements between and So for example lt 4 0 0 1 4 5 is a list containing six integers it is of type num There is an empty list denoted having the degenerate type void Unlike sets the order is maintained o 1999 Deloitte amp Touche Bakkenist ExSpect is a registered trade mark of ASPT 38 Deloitte amp Touche Bakkenist AN Tuple types Mapping types Record types ExSpect User Manual and no duplicates are removed So lt 1 2 3 lt 2 3 1 and lt 2 2 3 1 gt are all different The type A gt lt B contains value pairs the first from A the second from B They are represented as lt lt a b gt gt Here is the value constructor So for example 5 3 14 gt gt 1s a value from num gt lt real and lt lt a is from str gt lt str The and operators have priority over gt lt and gt so a set of pairs type needs brackets for example num gt lt str The type A gt B contains mappings finite sets of value pairs The values of this type can be constructed by combining the above two constructions A restriction is imposed though the first components from A have to be different
91. y basic str x converted to num utils divides the string y in a list of substrings e g words that are separated by a delimiter in symbols utils divides the string y in a list of substrings e g words that are separated by a space or by the characters basic str x converted to real utils string x in reverse order utils does x occur in y utils tail of y from first occurrence of x in y basic x converted to string utils are the first n characters of strings x and y the same utils length of string x basic string x without first character is a registered trade mark of ASPT 80 Deloitte amp Touche Bakkenist AN ExSpect User Manual 5 5 Tuple functions This section shows all tuple functions of the modules basic and utils upd x y EL E basic update x according to y 5 6 Product functions This section shows all product functions of the modules basic and utils pil x T gt lt S T basic first element of x pil x T gt lt S T utils yl y e T and exists ze S y z ex pi2 x T gt lt S 5 basic second element of x pi2 x T gt lt S S utils z ze S and exists ye T y gt lt z e x prod x T y S T gt lt S basic lt lt x y gt gt pair of x and y 5 7 Set functions This section shows all set functions of the modules basic and utils add x num y num num utils z ylzex add x real y real real utils z ylzex
92. y T T gt num bisect x T gt num y T gt num T gt num bjoin x T gt num y T gt num T gt num bjoin x T gt num T gt num bmax x num gt num num bmin x num gt num num bnull void gt num bocc x T gt num y T num botint x num num botint x real num bpick x T gt num T bproj x T gt num y T T gt num brest x T gt num T gt num bsize x T gt num num bsum x num gt num num btoset x T gt num ST bunion x T gt num y T gt num T gt num bunion x T gt num T gt num cat x str y str str cat x T y T T chisq n real seed real real chop x str n num str 1999 Deloitte amp Touche Bakkenist ExSpect ExSpect User Manual adt bag x with all elements of y added adt bag of all elements occurring in the sets in x adt bag x with one element y deleted adt bag x minus all elements of bag y adt 1s x an empty bag stat a random number bernouilli stat a random number binomial adt bag x with element y inserted adt biggest bag both contained in x and y bag intersection adt bag of all elements of x and y join adt bag of all elements of all bags in x join adt maximum greatest element of bag x adt minimum smallest element of bag x adt the empty bag adt number of times y occurs in bag x utils floor of x largest integer lt x basic floor of x largest integer lt x a

Download Pdf Manuals

Related Search

Related Contents

Mode d`emploi  Bedienungsanleitung ATLAS 500      Sony ICF-CD543RMSIL Operating Instructions  SW 700 P/B - SW 850 P/B SW 5070 P/B - SW 5080 P/B  Q - BMクリエーション  

Copyright © All rights reserved. Failed to retrieve file