Within the general system theory of Petri some means for modelling concurrent systems are provided. Cycloids belong to the fundamental building blocks to understand basic properties of systems. Up to now cycloids have a very limited scope with respect to general system properties. Valk's modelling proposals of circular tra c queues are rst valuable attempts to overcome these restrictions. In this contribution we extend the modelling in several ways. First of all we introduce con icts and other concepts to the modelling with cycloids. Second we use reference nets to increase expressibility of the modelling formalism, what eases the way to cover relevant system properties within the models while keeping relevant properties of the underlying processes of these models. As a result of both extensions we can express more interesting behaviour of concurrent systems. At the same time our construction of extended cycloids is designed in such a way that we can map our extended cycloid models to a set of cycloid models. In future work the transformation of Valk's formal results of the last years should be transferred to our extended versions.
Based on Minkowski's ideas about space and time [
The unit theory we sketched during the last years [
The extensions proposed here are still restricted with respect to general
systems of informatics. However, in [
In section 2 we discuss what kind of systems are covered by cycloids so far. Section 3 describes the kind of requirements we have for our intended cycloid applications. Section 4 contains a table of our currently covered extensions. Section 5 provides examples of the previous section. Section 6 covers ideas of our formal mapping of entities to cycloid models and the mapping of sets of cycloids to our extended cycloids. Section 7 relates our models to other kinds of modelling approaches like work ows, MAS and our unit theory. Section 8 summarises our results and sketches an outlook of further topics. 2
To illustrate what cycloids are and where their limits are we introduce some examples, formal de nitions and some descriptions. 2.1
Some prominent examples of cycloids by Petri are [
Based on this very symmetric model most discussions of cycloid behaviour
are made. However, already here the high symmetry of the model is
important.
{ The remen example where a group of remen extinguishes a re (and
repeats this in nitely often) (see example set of [
This kind of model is e.g. still an observable process. However, a reman
can move forward and backward exchanging full and empty buckets with a
neighbor. The gaps are xed, while the usage by the reman is not. This can
lead to di erent kinds of behaviour that are not covered in the formulas of
Valk [
Given ve (or more) gaps and two reman, one reman can be slow and move only between the rst two gaps while the second reman move very fast, performing all remaining movements over the remaining three (or more) gaps.
Furthermore, the reason for the reman is to exchange the full and empty buckets. This process of exchange is usually also not covered by the cycloid, since it is modelled implicitly.
Starting from these examples we provide our extensions. Before that we brie y sketch what cycloids are. 2.2
Cycloids are special Petri nets, more precisely the nets that can be expressed as a folding of a certain in nite Petri net. For the example of remen or cars that move through space and time Petri considered an in nite causal net that models the movement through space and time and the conditions of causality and concurrency. The in nite causal net is called Petri Space.
A concrete model can then be derived from the in nite net by folding it
with respect to four particular parameters ; ; and [
Figure 1 shows a cutout of the Petri space. The advance of time is depicted vertically and the advance of space is depicted horizontally. One can see that the cars travel forward in time and space whereas the gaps travel forward in time but backward in space.
To calculate cycloids the Petri space is folded by de ning an equivalence
relation. The quotient set of the equivalence relation on the Petri space will be
the set of net elements of the respective cycloid. The cycloid will have a nite
set of net elements since there is a nite number of equivalence classes for the
chosen model. Petri space elements in the same equivalence class will collapse
which can be seen as the literal folding of the in nite net. For a detailed coverage
of these notions we refer to [
The set of cars that drive within a xed set of driving slots is an example for a system that exhibits causality and concurrency. In the models that were considered so far it is only possible for a car to move forward if the driving slot in front of it is currently empty. We refer to these slots as gaps. In the real world it is possible for a car to move forward even if the slot in front of it is occupied if itself and the adjacent car accelerate simultaneously. However, this is not covered in cycloids, due to the concept of contact in the originally underlying Condition/Event-Nets (C/E-Nets).
Cycloids cover in nite behaviour with a nite set of actions. In our considered models we look at the behaviour as the possible actions of c cars and g gaps within c + g driving slots. These driving slots represent the sliding window that is currently looked at in a possibly bigger modelled world. Thus in our models the maximum distance between two cars is c + g 1. Another illustration is that the cars drive in a circuit of length c + g where they cannot overtake one another. If two cars are adjacent to each other the movement of the car in front (meaning that it has to leave the gap, hence releasing it for the next car, indicated by the marked gap place) is the condition for the car behind to be able to drive (causality). If two di erent cars have each a gap in front of them, they can drive forward independently (concurrency). A Petri net example which portrays a rst simple cycloid is shown in Figure 2. It is isomorphic to the net that is created by folding the Petri space with the parameters (2; 3; 1; 1) for ( ; ; ; ). The idea of cars and gaps will play a central role in providing examples for our simple extensions of cycloids which we will do in following sections.
Our considered models have got cyclic net structures. To avoid long and
possibly crossing edges in the straight depiction of the lanes we use virtual places
which are a feature of our Renew tool [
In the above sections we described what cycloids can do and already mentioned some limitations. This section addresses requirements for the extended cycloids.
First of all we want to decrease the size of the models when modelling
cycloids. A similar approach is presented by Valk [
Table 1. A table of our considered extensions
Expresses
Concurrency
Concurrency
Con ict
Con ict
Con ict
Con ict
Con ict
Con ict
Con ict
Coarsening
Con ict
Con ict
Distinctness
Distinctness
Con ict
Synchronization
Work ow
formulas as characterisations. Since we concentrate on the applicability of
cycloids for modelling we propose a subset of reference nets [
Second, we want to cover more concepts used in modelling. Therefore,
conicts are added. However, the idea is to restrict using them more or less as a
consistent extension of cycloids. In which ways this is possible and in which not
is discussed in the following sections. In the same context we introduce a
special variant of loops, motivated by work ow nets [
Table 1 contains our currently covered extensions. We will discuss examples for a selection of our extensions in section 5.
The model with m cars and n gaps on one lane is a simple example that can be expressed as a cycloid. It aids the intuitive understanding of causality and concurrency in distributed systems. Multiple independent lanes without the crossing of lanes increase the complexity of the model but since there are no conicts it can still be expressed as a cycloid. In our considered models we introduce con icts in di erent ways. For example, we add an overtaking bay of length one to the model of cars and gaps. This enables a particular car to overtake other cars which is not possible in traditional cycloid models. An overtaking lane of some length l allows for additional types of behaviour. In models that have an overtaking lane the cut in of the overtaking car can be prevented by another car if it stays in the driving slot intented for cut in. This will be ruled out in a model with guaranteed cut in. The overtaking lane can be unused if the cars do not decide to overtake other cars. We prevent this in a model with forced overtaking. Guaranteed cut in and forced overtaking can also be combined. One can also consider that multiple cars are able to move onto the overtaking lane or even are forced to do so. To describe a coarsened model one can de ne that multiple cars are able to be located at one driving slot. We model a scenario where an overtaking can begin on di erent driving slots but has always got a xed length. This will be called a sliding window. In a model with looser conditions the cars can freely switch between the lanes while they are moving forward. By modelling cars and/or gaps as coloured tokens, we are able to examine the properties of systems containing distinct cars and/or gaps. In the rst simple applications of cycloids the cars and gaps are indistinguishable. To further increase the complexity of the system and their models we introduce oncoming tra c on the additional driving lanes. Through the use of synchronous channels provided by the RENEW reference net formalism we model simultaneous actions of cars. Here the actions happen simultaneously in one simulation step. We also consider the presentation as a work ow by unwinding the conditions that regulate the behaviour of the net. 5 5.1
At rst we introduce a simple con ict by adding another lane to the model which is shown in Figure 3. Please note that the introduced con ict is modelled by virtual places. The lower part of the gure depicts the rst lane of driving slots. The upper part of the gure depicts the second lane which we will call the overtaking lane. The net model of each lane contains a row of place pairs which represent the driving slots. In the respective upper row places that represent cars are located, whereas the places the represent gaps are located in the lower rows. If a place representing a car is marked with a token it means that this driving slot is currently occupied by a car. If a place representing a gap is marked it means that this driving slot is not occupied. It makes sense that for each driving slot exactly one of the two places is marked. This is achieved by rst choosing an according initial marking of the net (which marks exactly one of the places). Futhermore, the two places for each driving slot are complementary places. This means that each transition that puts a token onto one of the places removes the token from the other one and vice versa. This property also ensures that for all reachable markings each place is marked with at most one token.
The initial marking of the net shows that there are four cars which are located in the rst four slots of the rst lane. There also is a gap in the fth slot. Remark that the overtaking lane has only got three driving slots since the places for the rst and last slot are virtual places of places that represent slots of the rst lane. There are no cars in the overtaking lane which is indicated by the three marked places representing the gaps.
There is cyclic behaviour in the system. For example the cars can drive behind each other in the rst lane. The introduced con ict shows when there is a car in the rst slot of the rst lane and also the second slot of the rst lane and the rst slot of the overtaking lane are currently empty. In this case the respective rst transitions of both lanes (rows) are activated. This means that the car in the rst slot of the rst lane can decide to either drive forward on the rst lane or to sheer out onto the overtaking lane. Having sheered out it can then overtake cars by moving forward on the overtaking lane. The fth slot of the rst lane is also used for cutting in from the overtaking lane which shows another con ict. In this model is it possible that multiple cars decide to move onto the overtaking lane. 5.2
One can imagine that the con ict at cutting in can be problematic in scenarios of the real world. For example, there can exist compulsive behaviour where one car is not letting another car cut in by blocking the slot used for cutting in. One motivation for modelling with cycloids is seeing them as a speci cation method for distributed systems. Here the behaviour of systems is described and speci ed with models that have got cyclic and also live behaviour. Liveness of system means that a continuous possibility of carrying out all the actions of the systems exists. This is a desired system property in many cases. Inspired by the MAS (multi agent system) context, it looks sensible to use cycloids for the speci cation of protocols that de ne the interaction of agents with other agents. The rules of a protocol ensure that the interaction of the agents leads to constructive behaviour. In the considered example of compulsive behaviour our rules should ensure that it will always be possible for a car to cut in after having sheered out. A reason for this condition in the real world can be that the overtaking lane ends because a section of no passing follows. If the cars on the rst lane block the overtaking car from cutting in it will have to wait on its lane. This will mean a loss of e ciency which should be prevented by specifying that only constructive behaviour should happen. We adapt the simple model shown in Figure 3 to prevent the unwanted compulsive behaviour and guarantee the cut in.
The Petri net model for guaranteed cut in is shown in Figure 4. The graphical representation is similar to Figure 3. The net contains a new place named 'mutex' which regulates a condition of mutual exclusion. The idea of the introduced condition is that cars are simply not allowed to move onto the slot used for cutting in while a car is currently located on the overtaking lane. If a car is currently located at the cut in slot, it is also not allowed for cars to enter the overtaking lane. In the net this is realized by making the mutex available initially which means that it is possible that either a car moves onto the cut in slot or a car moves onto the overtaking lane. In both cases the mutex is made unavailable by consuming the token in order to prevent the other action from happening. After a car leaves the cut in slot the mutex should be made available again. This is done by letting the transition responsible for leaving the cut in slot create a token on the mutex place. This construction leads to only one car being able to be located on the overtaking lane at the same time. 5.3
In Figure 3 we have seen that the cars can ignore the option to sheer out and drive forever on the rst lane which leaves the overtaking lane empty. This is not quite the behaviour that the modeller intended. We make another change to the net to change its behaviour. We want to achieve that in the case of an empty overtaking lane the rst car that is being able to sheer out onto the overtaking lane must do so and is not allowed to drive forward on the rst lane. We call this forced overtaking. We also want to enforce that if a car is currently located on the overtaking lane it is not possible for another car to enter the overtaking lane.
The Petri net model for forced overtaking is shown in Figure 5. In essence we still use the familiar color scheme. We introduce two new places that represent new conditions for regulating the overtaking behaviour of the cars. The place 'guard1' und its virtual places are drawn in yellow colour whereas the place 'guard2' and its copies are drawn in red colour. Initially the place 'guard2' (second guard) is marked whereas the place 'guard1' ( rst guard) is not. The rst lane initially has got four cars that are distributed on the rst four driving slots. The overtaking lane has got no cars initially. The two guards manipulate the behaviour of the two transitions that are in the postset of the place that models the car in the rst slot of the rst lane.
For this car to drive forward on the rst lane it is necessary that the rst guard is marked. This is the case if and only if a car is currently located on the overtaking lane. So for an empty overtaking lane it is forbidden to drive forward on the rst lane. If there is a car currently located on the overtaking lane and the rst guard is marked it will be allowed for the car to drive forward one the rst lane. In this case the token of the rst guard is consumed and created right after because the condition of the overtaking lane being not empty does not change. For a car on the rst slot of the rst lane to sheer out onto the overtaking lane it is necessary that the second guard is marked. This is the case if and only if no car is currently located on the overtaking lane. When sheering out, the corresponding transition consumes the token of the second guard and creates a token on the rst guard to update the current state of the conditions. When cutting in, the reverse actions happen. The token of the rst guard is consumed so cars on the rst slot of the rst lane are no longer able to drive forward on the rst lane and must sheer out again. Also a token is created on the second guard so cars are able to sheer out again. We see that there are three types of using the guards: Consuming the condition (removing the token), providing the condition (creating a token) or claiming the condition (needing but preserving the token). 5.4
So far, concurrent actions in our models can happen simultaneously in one
simulation step but can also happen after one another. We introduce further changes
to create a type of behaviour where it is forced that particular actions
happen in one simulation step. For this we use another concept of Renew, namely
synchronous channels. Synchronous channels consist of uplinks and downlinks.
Downlinks can be seen as transitions that are calling other transitions whereas
uplinks are the transitions being called. However, this metaphor is not exactly
correct since the transitions are carried out simultaneously which should not be
compared to a method call in programming. We will also use coloured tokens
which are supported by Renew as well. We remark here that it is also
possible to use multiple tokens on one place in other examples to portray coarsened
representations of bigger nets. We refer to [
Figure 6 shows a Petri net model with synchronized actions. We use the
metaphor that the fuel of the cars is running out as they drive. They have to
be refueled simultaneously. While the gaps in our model are still represented by
black tokens ([]), we use coloured tokens to model the cars. For futher information
concerning the use of coloured tokens in our modelling context we refer to [
The net has got no con icts and only one lane with ve driving slots. Initially there is a 'fuelfull' token on the two places representing the cars on the third and fourth driving slot, respectively. That means that initially there are cars with su cient fuel on the third and fourth driving slot. There are gaps on the other slots. When moving from the fth to the rst driving slot the type of the respective token changes from 'fuelfull' to 'fuelempty' by the corresponding action inscription. This is done by removing the 'fuelfull' token from the fth slot and creating a new 'fuelempty' token on the rst slot. In other cases 'fuelfull' tokens travel as 'fuelfull' tokens and 'fuelempty' tokens travel as 'fuelempty' tokens. A car that has not enough fuel to drive should not be able to move from the second to the third driving slot. In the net this is realized by adding the guard inscription 'guard x.equals("fuelfull")' to the 'b' transition. The guard states that the variable 'x' which is used for the transfer of tokens must be bound to a token of type 'fuelfull'. To continue driving the cars can get refueled by the two transitions depicted at the upper left hand area of the gure. These transitions carry the uplink inscriptions ':refuelA()' and ':refuelB()'. They each consume a 'fuelempty' token from the places that represent the rst two cars and create a 'fuelfull' token on them, respectively. This models the refueling of the cars. These two transitions are synchronized by the transition depicted above them which carries the two downlink inscriptions 'this:refuelA()' and 'this:refuelB()'. The inscriptions mean that of the current net instance which is referenced by the keyword 'this' the channels 'refuelA' and 'refuelB' are synchronized. After the cars have been refueled synchronously they can continue to drive.
In Figure 3 we see that the action of overtaking always begins at a xed slot and has got a xed length. We want to keep its xed length but let it begin at arbitrary slots. We call this idea sliding window. Figure 7 shows a model for a sliding window overtaking process. The model has got two lanes with ve slots each. Initially there are four cars on the rst four slots of the rst lane, whereas there are no cars located on the second lane. In essence the cars can freely switch between the two lanes if a corresponding gap exists at the moment. This is controlled by the ten transitions depicted at the middle of the gure. To enforce that a car cuts in at a certain slot after having sheered out we introduce ve new conditions that are represented by the places depicted in yellow, violet, orange, red and light color. These are unmarked initially. The conditions are provided when sheering out and consumed when cutting in. We choose a constellation in which a token is created on the place that needs to be marked for the respective car to cut in right after having sheered out. This leads to the sliding window having an overtaking length of one. However, unwanted behaviour still exists in the model. For example, if multiple cars switch to the overtaking lane the cut in slot to be enforced is not mapped to the sheered out car which enables one of the cars to use the cut in slot being enforced for the other one. Also the cars can stay on the overtaking lane forever and choose to never cut in the rst lane again. 5.5
We also show a presentation as a work ow by rst unwinding the conditions of the Petri net model and then transforming the emerging net into a work ow Petri net. We consider a example wherein the maximum distance of two driving cars is ve which means that there are six driving slots. In this example we have got two cars. Initially the two cars are located on two arbitrary slots that are adjacent to each other (so they have got a distance of one unit).
The Figure 8 shows a cutout of the causal net that emerges from unwinding the following conditions. Again we use the colour scheme of blue and grey. In order to get a work ow Petri net we add a start place and an end place together with the respective forking and joining transitions. This is depicted in Figure 9.
First of all the car in front needs to move forward to enable the car behind it to move as well. This is modelled by the six gaps that are next to each other in the graphical depiction. Secondly, since the maximum distance must not exceed the value of ve slots the car behind needs to move forward before the movement of the car in front would cause the distance between them to exceed ve driving slots. This is modelled by the two gaps located at the upper area of the graphical depiction. It is worth to see that the maximal distance can in some circumstances be larger in Figure 8, when the car behind has proceeded by two gaps. Then the car in front can move until it has to wait again for the car behind. This behaviour is not possible in Figure 9. Start and end places restrict the possible behaviours. Since e.g. in our MAS models we require to have such starting and ending condition for one of the conversations of two agents, this is not always problematic. What is gained by the restriction is a better understandability of behaviours. One has to start in a single precisely de ned initial state and then, after the synchronisation via the end place can restart.
After the discussion of extension options above we now discuss the mapping of modelling entities to extended cycloids and of extended cycloids to traditional cycloids. In this section we restrict ourselves to the informal motivation of the mappings. These mappings are most often straight forward, so that we do not provide a formalization. First of all the extension by the use of reference nets needs to be discussed. Second the additional concepts of con ict (and (for-)loops) are treated.
Using virtual places is well known from other formalisms like Coloured Petri
Nets [
Other shortcuts like the colouring of tokens and the use of variable is nicely
demonstrated by the results of Valk in [
When cars need di erent treatment, e.g. a police car that must have to option to overtake and enforce its cut in, than we need to re ect this in the model. This is covered by the di erent version we show in Section 5.
Another scenario not discussed before here is that the overtaking of autonomous driving cars can be speci ed as a kind of required behaviour. Interpreting the overtaking model a speci cation and ensuring that only correct and complete overtaking scenarios are allowed by the (extended) cycloid, we can ensure that the action of overtaking is safe (if no breakdown of the hardware occurs). An overtaking car can bypass a certain number of cars and then sheer in again before cars on the other lane can collide with them.
Actually when modelling the car on the other lane that approaches a convoy from the opposite direction there is a certain number of free gaps for the overtaking actions. If and only if the speed and the number of gaps is su cient a car may overtake the other cars.
Modelling extended cycloids to (traditional) cycloids like those used by Petri
or in [
Following the nite set of actions of a modelled system this implies that if the number of actions within a given scenario at least one action must be used more than once. For in nite scenarios this is obvious. Good systems (designed following the ideas of being a correct work ows for each work ow of a system) should react to an external stimuli like a message and then remain in a state until the next external event occurs. This is an ideal scenario, but it allows to specify a reaction of a system more easily. Interference of several concurrent events that have con icts with respect to actions of resources are explicitly prohibited in our kinds of system models. This restricts the systems that can be modelled, but due to the inclusion of con icts it still can cover more processes than a traditional cycloid.
However, one can consider the extended cycloid as a kind of description of several cycloids. Each cycloid has an initial marking from which it can perform a certain set of actions until it starts in the beginning again.1
Now, if there is exactly a single place with two transitions in con ict within a model then this only describes two di erent cycloid structures that may be used. Given that one alternative is never used than exactly the normal cycloid could be used for its description. The same holds for the other alternative. Both cycloids can be considered to describe the behaviour of a system or unit. The only di erence lies in that part of the process that re ects the selection of the alternative. When considering a cycloid model as the blueprint for a unit then the cyclic behaviour can be seen as a composition of processes of this unit. What needs to be seen here is, that the possible behaviours can change, since the possible distances between tokens can be increased due to the larger model structure.
In the case that there is an alternative in the system structure then for each alternative there is di erent unit that can be used to generate the corresponding process. In some way we have used this technique when we developed the Petri net protocols for our Petri net based multi-agent systems. First models just described a concurrent behaviour of two or more agents interacting. This exactly re ects a cycloid structure. When agents repeat this behaviour then this results in the cycloid process.
To increase the modelling power of our agent protocol modelling technique we introduced alternative. The same was added by the AUML approach of James 1 This is a simpli cation, however, the number of variants is strictly limited due to the fact that there is a maximal possible distance between the rst and the last token within a cycloid.
When using the idea of work ows with a single initial marking and a single end
marking place, then this is easy to see. Nevertheless this is not so simple in the
general case for cycloids, since the initial marking is normally larger than a single
token.
Odell et al [
For this contribution it is important to notice that we can either assume that we describe a net structure without alternatives to form a basic unit of behaviour. The concatenation of the structure, the unfolding with respect to a given initial marking, results in uniform behaviour that can be described by a cycloid. Adding alternatives within the structure can be seen as the option to concatenate some variants units to form the behaviour.
The other modelling perspective is to look at process and fold these process
to structures, as it is done by Petri with his Petri space. The folding can be done
for the simple model of cars and gaps for the dimension of space of time. Folding
both results in the cycloid. More complex models that have more than two
dimensions. These kind of models have been considered in the thesis of Fenske
[
An interesting perspective is to not use process and fold them to cycloids, but
to use branching process and fold them to our extended cycloids. For a restricted
set of branching process (with a nite set of regular behaviour patterns) this
should be no problem using our proposed mapping. The composition as already
used by Valk in [
Compared to the above proposals some modelling approaches were motivating the extensions. In general repetitive behaviour is assumed. This can be found in may application areas of informatics.
Building applications is normally designed for certain scenarios [
Our proposals of some bounded set of possible behaviours is of course also
followed in many other modelling approaches. UML (Uni ed Modeling
Language) with its various modelling techniques, BPMN (Business Process Model
and Notation) or other Petri net formalisms and restrictions of Petri nets like
work ows use in their methods the idea of simple behaviours that can be
executed repetitively. The same holds for multi-agent systems where agents inherit
some kinds of behaviour. Usually this behaviour is triggered from the outside
and should terminate after the external stimulus or message has been processed.
In our Mulan framework this is nicely covered. Due to the usage of higher
inscriptions languages like Java again the MAS modelling becomes turing
complete. Especially the possibility of self-adaptation (see e.g. [
Cycloids provide the means for a single scenario with in fact certain basic
blocks of repeated behaviours. There is always a nite number of di erent
marking in a cycloid. Only the variations of such markings provided the possibly
in nite number of process that can be build from an initially marked cycloid.
Correct work ows [
Our extensions more or less adds some further kinds of markings of a set of places. However, the modellers can use con icts or for loops, what ensures that the number of possible markings remain nite. In addition to the cycloids now not all transitions within an extended cycloid will re when an initial marking is reached. Obviously alternatives hinder such rings. The same holds if a loop is skipped due to a possibly false condition from the beginning onwards.
With respect to the unit theory a unit describes a any kind of system (see
e.g. [
Modelling repeated behaviour is demanding. As a simple solution cycloids were developed. Restrictions with respect to the modelling power inspired us to extend the cycloids.
The extension were done in two di erent directions. First new concepts were added to the model more complex systems. Especially con icts need to be mentioned here. Second reference nets are used to build the models. Using reference nets allows to build more complex models. Applying restrictions on the usage of colours, synchronous channels and other constructs leads to the possibility to map the coloured models to the extended cycloids which again can be somehow described by sets of cycloids.
Future work needs to address the provision of closed formulas as this was done during the last years by Valk. Relations to work ow modelling and other modelling areas like MAS are highly promising. Overall we are sure that the results can be used to provide a formal basis for some parts of the unit theory.
Starting from [
Computer scientists, software engineers and other people of informatics urgently need better modelling techniques. Extended cycloids are one option to provide a solid basis on the ground of concurrency theory for more expressive modelling techniques for application areas where a xed set of scenarios need to be covered in formal manner.