AsmetaL — Reference Guide

March 2026

The AsmM concrete syntax (AsmetaL) is a textual notation to be used by modelers to effectively write ASM models within the ASMETA framework. It is defined in terms of an EBNF (extended Backus-Naur Form) grammar derived from a semantic interpretation of the AsmM metamodel (the abstract syntax).

The AsmetaL language can be divided roughly into four parts: the structural language (provides the constructs required for describing the structure of an ASM model.), the definitional language (provides the basic definitional elements such as functions, domains, rules and axioms characterizing an algebraic specification), the language of terms (provides all kinds of syntactic expressions which can be evaluated in a state of an ASM), and the behavioral language or the language of rules (provides a notation to specify the transition rule schemes of an ASM).

This quick guide gives a description of each part by presenting the notation in an intuitive style for better readability, instead of reporting the grammar productions. For a more formal definition see the EBNF grammar.

Note that, to write an ASMETA model of a system, the file containing the ASMETA specification must contain a single ASM structure definition and take the .asm extension (e.g. MyAsmModel.asm).

Notational Conventions

In this guide the following conventions are adopted:

• the AsmM concrete syntax appears in violet text

• keywords appear in bold face

• a pair of square braces (not in bold face) is not considered part of the concrete notation, it indicates only that the enclosed expression is optional

• the notation as in t1,…,tn indicates one or more elements.

Syntactic rules on ID names

We use the following rules to distinguish among names of domains, functions, enumeration elements, rules, variables:

ID_VARIABLE a string beginning with the dollar sign “$”; e.g. $x $abc

ID_ENUM a string of length greater than or equal to two and consisting of upper-case letters only; e.g. ON OFF RED

ID_DOMAIN a string beginning with an upper-case letter; e.g. Integer X SetOfBags Person

ID_RULE a string beginning with the lower-case letter “r” followed by the underscore symbol “_”; e.g. r_SetMyPerson r_update

ID_FUNCTION a string beginning with a lower-case letter, but not starting with “r_”; e.g. plus minus re

Comments

Comments can be written as follows:

// text to be commented

/* text to be commented*/

Structure of an ASMETA model

An ASMETA model is structured into four sections: a header, a body, a main rule, and an initialization.

This example defines a simple ASMETA model of a counter that ranges from 0 to 60.

asm counter 

//Header
import StandardLibrary 

signature:
 domain Sixty subsetof Integer
 controlled count: Integer

//Body
definitions:
domain Sixty = {0 : 60}

macro rule r_Increment =
 count := count + 1

//Main rule
main rule r_Main =
 if count = 60 then
   count := 0
 else
  r_Increment[]
 endif

//Initialization
default init s0:
 function count = 0

In the following, we analyze each component of the ASMETA model in detail.

ASMETA declaration

[asyncr] asm name

• name is the name of the ASMETA model. It must be equal to the name of the file (as name.asm).
• asyncr keyword specifies if the ASM is an asynchronous multi-agent or not. If omitted, the ASMETA model is considered a synchronous multi-agent.

Header

Import/Export

[ import m₁ [( id₁₁,...,id₁ₕ₁ )]
 ...
 import mₖ [( idₖ₁,...,idₖₕₖ )]
]
[ export id₁,...,idₑ ]  or   [ export * ]

• m₁,…,mₖ are the names of the imported modules

• idᵢ₁,…,idᵢₕᵢ are names for domains, functions, and rules which are imported from module mᵢ (if they are omitted, all the content of the export clause of mi is imported);

• id₁,…,idₑ are names for domains, functions, and rules which can be exported from the ASMETA model.

  export* denotes that all functions and rules of the ASMETA model can be exported;

Tip

When importing another asmeta file, one can use either the relative or absolute path, with or without the asm extension. In case the path contains spaces, the use of quotes “ to delimit the path is mandatory. Examples:

import ../myotherfile
import ../libs/library.asm
import "C:Users/user/my asms/asm1.asm" 

Signature

signature:
 [ dom_decl₁ ... dom_declₙ ]
 [ fun_decl₁ ... fun_declₘ ]

• dom_decl₁,…,dom_declₙ are declarations of domains used in the ASM (see section Domain declarations);
• fun_decl₁,…,fun_declₘ are declarations of functions used in the ASM (see section Function declarations).

Body

definitions:

Domain Definitions

[ domain D₁ = Dterm₁ …
domain Dₙ = Dtermₙ ]

• D₁,…,Dₙ are names of static concrete domains declared in the signature (see Header);
• Dterm₁,…,Dtermₙ are terms (see section Terms).

Function Definitions

[ function F₁ [( p₁₁ in d₁₁,…,p₁ₖ₁ in d₁ₖ₁ )]= Fterm₁ …
function Fₙ [( pₙ₁ in dₙ₁,…,pₙₖₙ in dₙₖₙ )]= Ftermₙ ]

• F₁,…,Fₙ are names of static or derived functions declared in the signature (see Header);*
• pᵢⱼ are variables which specify the formal parameters of the function Fᵢ, and dᵢⱼ are the domains where pᵢⱼ take their value;
• Fterm₁,…,Ftermₙ are terms (see section Terms).

Macro Rule Definitions

[ [macro] rule R₁ [( x₁₁ in b₁₁,…,x₁ₖ₁ in b₁ₖ₁ )] = rule₁ …
[macro] rule Rₙ [( xₙ₁ in bₙ₁,…,xₙₖₙ in bₙₖₙ )] = ruleₙ ]

• R₁,…,Rₙ are names for macro rules;
• xᵢⱼ are variables which specify the formal parameters of the macro rule Rᵢ, and bᵢⱼ are the domains where xᵢⱼ take their value;
• rule₁,…,ruleₙ are transition rules (see section Transition rules);

Turbo Rule Definitions

[ turbo rule TR₁ [( x₁₁ in b₁₁,…,x₁ₖ₁ in b₁ₖ₁ )] [in b₁] = rule₁ …
turbo rule TRₙ [( xₙ₁ in bₙ₁,…,xₙₖₙ in bₙₖₙ )] [in bₓ]= ruleₙ ]

• TR₁,…,TRₙ are names for turbo rules;
• xᵢⱼ are variables which specify the formal parameters of the turbo rule TRᵢ, and bᵢⱼ are the domains where xᵢⱼ take their value;
• bᵢ are domains where the return values of turbo rules (with return value) range;
• rule₁,…,ruleₙ are transition rules (see section Transition rules).

Invariant Definitions

[ invariant I₁ over id₁₁,…,id₁ₛ₁ : term₁ …
invariant Iₙ over idₙ₁,…,idₙₛₙ : termₙ ]

• I₁,…,Iₙ are names for invariants;
• idᵢⱼ are names of domains, functions (when functions are overloaded, it is necessary to indicate their domain, as in f(d)with f the function name and d the name of the function domain), and rules constrained by the invariants;
• term₁,…,termₙ is a term (see section Terms) representing the boolean-valued expression of the constraint.

Temporal Logic Properties

[ TLPROP name₁ over id₁ᵢ,…,id₁ₙ: term₁ ...
 TLPROP nameₙ over idₙₙ,…,idₙₘ: termₙ ]

• name₁,…,nameᵢ are names for the properites;
• idₙⱼ are names of domains, functions (when functions are overloaded, it is necessary to indicate their domain, as in f(d) with f the function name and d the name of the function domain), and rules constrained by the property;
• term₁,…,termₙ are terms (see section Terms) representing the boolean-valued expression of the constraint.
• TLPROP is one of:
  • CTL properties:

  [ CTLSPEC | ctlspec ]
  

  • LTL properties:

  [ LTLSPEC | ltlspec ]
  

  • A justice constraint consists of a formula f, which is assumed to be true infinitely often in all the fair paths:

  [ JUSTICE | justice ]
  

  • It indicates a justice constraint as well (in NuSMV it has been kept for backward compatibility):

  [ FAIRNESS | fairness ]
  

  • A compassion constraint consists of a pair of formulas (p,q); if property p is true infinitely often in a fair path, then also formula q has to be true infinitely often in the fair path:

  [ COMPASSION | compassion ]
  

  • Invariants (assumptions about the state):

  [ INVAR | invar ]
  

Important

To write temporal logic properties, it is necessary to import the proper library and use the temporal operators defined in that library.

Main

main rule R = rule₁

• R is the name of the main rule;
• rule₁ is a transition rule (see section Transition rules).
• If the ASMETA model has no main rule, as a default, the simulator starts executing in parallel the agent programs as specified by the agent initialization clauses (see initializations) in the initial state.

Initialization

[ init I₁ :
      [  domain D₁₁ = Dterm₁₁  ...
         domain D₁ₙ₁ = Dterm₁ₙ₁
      ]
      [  function F₁₁ [(  p₁₁ in d₁₁,...,p₁ₛ₁ in d₁ₛ₁ )]= Fterm₁₁ ...
         function F₁ₘ₁ [( pₘ₁₁ in dₘ₁₁,...,pₘ₁ₛₘ₁ in dₘ₁ₛₘ₁ )]= Fterm₁ₘ₁
      ]
      [  agent A₁₁ : r₁₁  ...
         agent A₁ᵤ₁ : r₁ᵤ₁
       ]
  ...
]
default init Iₓ :
      [  domain Dₓ₁ = Dterm₁₁ ...
         domain Dₓₙₓ = Dtermₓₙₓ
      ]
      [  function Fₓ₁ [( p₁₁ in d₁₁,...,p₁ₛ₁ in d₁ₛ₁ )]= Ftermₓ₁ ...
         function Fₓₘₓ [( pₘₓ₁ in dₘₓ₁,...,pₘₓₛₘₓ in dₘₓₛₘₓ )]= Ftermₓₘₓ
      ]
      [
         agent Aₓ₁ : rₓ₁ ...
         agent Aₓᵤₓ : rₓᵤₓ
      ]
[ ...
   init Iₜ :
       [ domain Dₜ₁ = Dtermₜ₁ ...
         domain Dₜₙₜ = Dtermₜₙₜ
       ]
       [  function Fₜ₁ [( p₁₁ in d₁₁,...,p₁ₛ₁ in d₁ₛ₁ )]= Ftermₜ₁ ...
          function Fₜmₜ[( pₘₜ₁ in dₘₜ₁,...,pₘₜₛₘₜ in dₘₜₛₘₜ )] = Ftermₜₘₜ
       ]
       [  agent Aₜ₁ : rₜ₁ ...
          agent Aₜᵤₜ: rₜᵤₜ
       ]
]

• I₁,…,Iₓ,…,Iₜ are names for the initial states of the ASM;
• the default initial state Iₓ is compulsory;
• Dᵢⱼ are names of dynamic concrete domains, already declared in the signature (see Header) and initialized in the initial state Iᵢ;
• Fᵢⱼ are names of dynamic functions, already declared in the signature (see Header) and initialized in the initial state Iᵢ;
• pᵢⱼ are variable terms which specify the formal parameters of the corresponding function, and dᵢⱼ are the domains where pᵢⱼ take their value;
• Ftermᵢⱼ e Dtermᵢⱼ are terms (see section Terms) specifying the initial value for the function Fᵢⱼ and domain Dᵢⱼ;
• Aᵢⱼ and rtut are agent domains (concrete sub-domains of the Agent type-domain) and rules assigned as programs to the agents, respectively. If no agent initialization clause is specified, by default, the ASM is assumed to be single-agent and the program and the identifier of the unique agent are respectively the ASM’s main rule (see Main rule) and the ASM’s name.

ASMETA module

A lightweight notion of module is also supported. An ASMETA module is an ASMETA model without the main rule and the initialization. We write a module in the same way as ASMETA model, with the keyword asm replaced by the keyword module.

module name

where name is the name of the ASMETA module. It must be equal to the name of the ASMETA file (as name.asm).

This example defines a simple ASMETA model of a counter that ranges from 0 to 60 by introducing a module.

module counterModule 

//Header
import StandardLibrary 

signature:
 domain Sixty subsetof Integer
 controlled count: Integer

//Body
definitions:
domain Sixty = {0 : 60}

macro rule r_Increment =
 count := count + 1

asm counter 

//Header
import counterModule 

signature:
 
//Body
definitions:

//Main rule
main rule r_Main =
 if count = 60 then
   count := 0
 else
  r_Increment[]
 endif

//Initialization
default init s0:
 function count = 0

ASMETA Standard Libraries

In ASMETA, libraries are predefined ASMETA modules that can be imported into your models to reuse common definitions and extend the language with additional functionality. They typically contain:

• domains
• functions
• rules Using libraries helps avoid redefining standard elements and simplifies model development.

StandardLibrary.asm

This is the core library and is almost always required. It provides:

• standard domains (e.g., Integer, Boolean)
• basic operators (arithmetic and logical)
• commonly used functions

LTLLibrary.asm and CTLLibrary.asm

These libraries are used for formal verification with the model checker:

• LTL (Linear Temporal Logic): used to express properties over execution traces
• CTL (Computation Tree Logic): used to express properties over branching execution paths They allow you to specify temporal properties.

TimeLibrary.asm and TimeLibrarySimple.asm

TimeLibrary introduces the concept of time into ASMETA models. It provides:

• time-related variables
• functions for handling time
• support for modeling time-dependent behavior

TimeLibrarySimple is a simplified version of TimeLibrary. It offers:

• basic time-related features
• easier usage compared to the full TimeLibrary
• Note: this library is considered experimental.

All the libraries, if necessary, must be imported into the ASMETA model:

import StandardLibrary
import LTLLibrary
import CTLLibrary
import TimeLibrary
import TimeLibrarySimple

Domain declarations

The ASMETA domains (or universes) are classified into: typedomains and concrete-domains.

The type-domains represent all possible super domains (for practical reasons, the superuniverse |S| of an ASM state S is divided into smaller universes) and are further classified in:

• basic type-domains, domains for primitive data values like booleans, reals, integers, naturals, strings, etc.;
• structured type-domains, domains for building data structures (like sets, sequences, bags, maps, tuples etc.) over other domains;
• abstract type-domains, dynamic user-named domains whose elements have no precise structure and are imported as fresh elements from a possibly infinite reserve by means of extend rules (see section Transition rules);
• enum domains, finite user-named enumerations to introduce new concepts of type (e.g. one may define the enumeration Color = {RED, GREEN, BLUE} to introduce the new concept of “color”).

Concrete domains are user-named sub-domains of type-domains. As for functions, a concrete domain can be static or dynamic.

The schema below shows the notation for declaring a domain. Domains declared as anydomain are generic domains representing any other type-domain. The standard library defines one “predefined” anydomain, named Any, which represents the most generic one. As basic type-domains only Complex, Real, Integer, Natural, String, Char, Boolean, Rule, and the singleton Undef={undef} are allowed and defined in the standard library as predefined basic type-domains. Moreover, two other special abstract domains are considered predefined: the Agent domain for agents, and the Reserve domain, which works as “reserve” to increase the working space of an ASM. Note that the Reserve domain is considered abstract, and therefore dynamic, since it is updated automatically upon execution of an extend rule (see section Transition rules) – it can not be updated directly by other transition rules.

Any Domain

anydomain D

• D is the name of the domain representing any other type-domain.
• A predefined generic domain named Any is declared in the standard library and considered the most generic one.

Basic Domain

basic domain D

Only Complex, Real, Integer, Natural, String, Char, Boolean, Rule, and Undef are allowed (users can not define other basic domains). They are declared in the standard library as “predefined” basic type-domains.

Abstract Domain

abstract domain D

• D is the name of the type-domain.

Example

abstract domain Lift

Enumerative Domain

enum domain D = { EL₁|...|ELₙ }

or

enum domain D = { EL₁,...,ELₙ }

• D is the name of the enum type-domain;
• EL₁,…,ELₙ are the elements of the enumeration which must be written in all caps.

Example

enum domain Sign = {CROSS | NOUGHT}
enum domain Status = {TURN_USER, TURN_PC}

The Sign domain contains CROSS and NOUGHT as elements of the domain. The Status domain contains TURN_USER and TURN_PC as elements of the domain.

Concrete Domain

[ dynamic ] domain D subsetof td

• D is the name of the concrete domain to declare;
• td is a type-domain which identifies the structure of the elements of the declared concrete domain;
• the keyword dynamic denotes that the declared domain is dynamic. If omitted, the domain is considered static.

Example

domain Coord subsetof Integer

The Coord domain contains a subset of elements taken from the Integer basic domain. The definition of the elements in the Coord domain is done in the definitions section.

Product Domain

Prod ( d₁,d₂,...,dₙ )

• d₁,d₂,…,dₙ are the domains over which the Cartesian product is defined.

Example

domain Position subsetof Prod(Coord, Coord)

The Position domain is defined over the Cartesian product of the Coord domain. If we consider that the elements of Coord are {1,2,3}, the elments of domain Position are {(1,1),(1,2),(1,3),(2,1),(2,2),(2,3),(3,1),(3,2),(3,3)}.

Sequence Domain

Seq ( d )

• d is the domain over which the sequence domain is defined. It is an ordered collection of elements belonging to the domain d.

Example

domain Plan subsetof Seq(Position)

The Plan domain is a finite sequence of elements defined in the Position domain. If we consider that the elements of Position are {(1,1),(1,2),(1,3),(2,1),(2,2),(2,3),(3,1),(3,2),(3,3)}, the elements of domain Plan can be, for example, ((1,1),(1,2),(2,2)}, {(2,2),(2,3),(3,1),(3,3)).

Powerset Domain

Powerset ( d )

• d is the domain over which the power set domain is defined. It is the set of all subsets of a given base domain.

Example

domain SignCombination subsetof Powerset(Sign)

The SignCombination domain contains the set of all subsets of the Sign domain. If we consider that the elements of Sign are {CROSS | NOUGHT}, the elements of the domain SignCombination are {}, {CROSS}, {NOUGHT}, {CROSS, NOUGHT}.

Bag Domain

Bag ( d )

• d is the domain over which the bag domain is defined. It is an unordered collection of elements where an element can appear more than once.

Example

domain ListOfStudentGrade subsetof Bag(Grade)

The ListOfStudentGrade domain contains an unordered collection of elements from the Grade domain. If we consider that the elements of Grade are {0,1,2,3,4,5}, the elements of the domain ListOfStudentGrade can be, for example, {4,5,4,3,5}.

Map Domain

Map ( d1,d2 )

• d1,d2 are the domains over which the map domain is defined. It is a structured domain used to represent a mapping from a key domain to a value domain, effectively functioning as a mathematical map or dictionary.

Example

domain CourseGrade subsetof Map(Course, Grade)

The CourseGrade domain contains a map from elements in the Course domain to elements in the Grade domain. If we consider that the elements of Grade are {0,1,2,3,4,5} and elements of Course domain are *{MATHS, ARTS, SCIENCE}, the elements of the domain CourseGrade can be, for example, {(MATHS,5), (ARTS,5), (SCIENCE,4)}.

Function Declarations

To declare an ASMETA function, it is necessary to specify the name, the domain, and the codomain of the function.

The schema below shows the concrete syntax for declaring a function F (the name) from D (the domain) to C (the codomain). 0-ary functions (state variables) have only the codomain.

Static Function

static F : [ D -> ] C

A static function F is a function whose value is fixed and does not change during execution. It is defined in the definitions section. static functions cannot contain in their definition dynamic or derived functions.

Examples

signature:
 static maxValue: Integer

definitions:
 function maxValue = 60

The static function maxValue is a constant and always evaluates to 60.

signature:
 static max: Prod(Integer,Integer) -> Integer

definitions:
 function max ($a in Integer, $b in Integer)= ...

The static function max given two integers returns the maximum of them.

Dynamic Function

[ dynamic ] ( monitored | controlled | shared | out | local ) F : [ D -> ] C

A dynamic function F is declared specifying its kind (monitored, controlled, shared, or out); optionally, the keyword dynamic can also be added as a prefix. Local dynamic functions can be declared only in the scope of a turbo transition rule with local state (see section Transition rules).

Monitored Function

A monitored function represents an input coming from the environment. Its value is not controlled by the system but can change nondeterministically.

Controlled Function

A controlled function represents a system variable whose value can be modified by the system through rules. Its value evolves during execution.

Shared Function

A shared function is used to model interaction between multiple agents, where more than one entity may read or update its value.

Output Function

An output function represents values produced by the system and visible to the environment.

Example

asm AutomaticDoor

import StandardLibrary

signature:
 controlled doorOpen: Boolean //true: the door is open, false: the door is closed
 monitored motionDetected: Boolean //true: there is a person in front of the dor
 shared peopleCount: Integer //number of people entered in the room
 out doorStatus: String // Out message

definitions:
 main rule r_Main =
  if motionDetected then
   par
    doorOpen := true
    peopleCount := peopleCount + 1
    doorStatus := "open - number of people in the room: " + toString(peopleCount+1) 
   endpar
  else
    if peopleCount=0 then
     par
      doorOpen := false
      doorStatus := "closed"
     endpar
    endif
  endif

default init s0:
 function doorOpen = false
 function peopleCount = 0

The system opens the door upon motion detection and increments the people count; otherwise, if no motion is detected and the area is empty, the door closes, and the output reflects the door state.

Derived Function

derived F : [ D -> ] C

derived functions are computed from other functions; they can contain in their definition both static and dynamic (and derived) functions (but they must contain at least a dynamic function). dynamic functions are re-evaluated at each state.

Examples

 signature:
 controlled x: Integer
 controlled y: Integer
 derived sum: Integer

definitions:
 function sum = x + y

The function sum is derived from x and y. It is automatically updated whenever x or y changes.

signature:
 controlled grade: Integer -> Integer
 derived passed: Integer -> Boolean

definitions:
 function passed($g in Integer) =
  grade($g) >= 18

The value of the function passed is true, if the student grade is >= 18.

Terms

There are two types of terms, basic terms as in first-order logic (variables, constants and function applications) and extended terms to represent special terms like tuple terms, collection terms (sets, maps, sequences, bags), the conditional term, variable-binding terms, etc.

Basic Terms

Extended Terms

Standard Operators

In addition to these terms, the AsmM concrete syntax admits special expressions to support the infix notation for some well-known functions on basic domains (like plus, minus, mult, etc.) of the AsmM Standard Library. In these expressions, basic terms and the domain term are used as operands. The table below show the infix operators corresponding to these functions, together with their associativies and priorities. The operator priorities range from 0 to 9, where 9 indicates the strongest one and 0 the weakest one.

Transition Rules

In a given state, a transition rule of an ASM produces for each variable assignment an update set for some dynamic functions of the signature. We classify transition rules in two groups: basic rules and turbo rules. The former are simply rules, like the skip rule and the update rule, while the latter are rules, like the sequence rule and the iterate rule, introduced to support practical composition and structuring principles of the ASMs. Other rule schemes are derived from the basic and the turbo rules.

SkipRule

skip

The skip rule, when executed, does not update any function, and the system state remains unchanged.

UpdateRule

l:=t

where:

• t is a generic term.
• l can be either a location term f(t1,…,tn) or a location variable (like $x).

Example

signature:
  controlled counter: Integer

definitions:
  main rule r_Main =
    counter := counter + 1

default init s0:
	function counter = 0

The value of counter function is incremented by 1 at each step.

BlockRule

par
  R1 R2 ... Rn
endpar

• R1,R2,…,Rn are transition rules executed simultaneously (in parallel).

Example This model describes a system in which the value of a controlled counter is updated based on an external input.

signature:
  monitored userchoice: Integer
  controlled counter: Integer
  out message: String

definitions:
  main rule r_Main = 
    par
      counter := counter + userchoice
      message := "Counter increased by " + toString(userchoice)
    endpar

default init s0:
	function counter = 0

The monitored function userchoice represents a value provided by the environment. At each execution step, the system increases the controlled function counter by the value of userchoice and updates the output function message to reflect the performed increment.

ConditionalRule

if G then Rthen [else Relse] endif

• G is a term representing a Boolean condition.
• Rthen and Relse are transition rules. If Relse is omitted, it is assumed else skip as default.

Example These models describe a system in which the value of a controlled counter is updated based on an external input.

signature:
  monitored userchoice: Integer
  controlled counter: Integer
  out message: String

definitions:
  main rule r_Main = 
    if counter > 10 then
      par
        counter := counter + userchoice
        message := "Counter increased by " + toString(userchoice)
      endpar
    endif

default init s0:
	function counter = 0

The monitored function userchoice represents a value provided by the environment. At each execution step, if the userchoice function is greater than 10, the system increases the controlled function counter by the value of userchoice and updates the output function message to reflect the performed increment.

signature:
  monitored userchoice: Integer
  controlled counter: Integer
  out message: String

definitions:
  main rule r_Main = 
    if counter > 10 then
      par
        counter := counter + userchoice
        message := "Counter increased by " + toString(userchoice)
      endpar
    else
      par
        counter := counter - userchoice
        message := "Counter decreased by " + toString(userchoice)
      endpar
    endif

default init s0:
	function counter = 0

The monitored function userchoice represents a value provided by the environment. At each execution step, if the userchoice function is greater than 10, the system increases the controlled function counter by the value of userchoice and updates the output function message to reflect the performed increment; otherwise the system decreases the controlled function counter by the value of userchoice and updates the output function message to reflect the performed decrement.

Reference Card