P Expressions
A Function in P can be arbitrary piece of imperative code which enables programmers to capture complex protocol logic in their state machines. P supports the common imperative programming language expressions (just like in Java).
P Expressions Grammar
expr :
| (expr) # ParenExpr
| primitiveExpr # PrimitiveExpr
| formatedString # FormatStringExpr
| (tupleBody) # TupleExpr
| (namedTupleBody) # NamedTupleExpr
| expr.int # TupleAccessExpr
| expr.iden # NamedTupleAccessExpr
| expr[expr] # AccessExpr
| keys(expr) # KeysExpr
| values(expr) # ValuesExpr
| sizeof(expr) # SizeofExpr
| expr in expr # ContainsExpr
| default(type) # DefaultExpr
| new iden ( rvalueList? ) # NewExpr
| iden ( rvalueList? ) # FunCallExpr
| (- | !) expr # UnaryExpr
| expr (* | / | + | -) expr # ArithBinExpr
| expr (== | !=) expr # EqualityBinExpr
| expr (&& | ||) expr # LogicalBinExpr
| expr (< | > | >= | <= ) expr # CompBinExpr
| expr as type # CastExpr
| expr to type # CoerceExpr
| choose ( expr? ) # ChooseExpr
;
# Formated strings for creating strings
formatedString
| format ( StringLiteral (, rvalueList)? )
;
primitiveExpr
: iden # Identifier
| FloatLiteral # FloatConstant
| BoolLiteral # BooleanConstant
| IntLiteral # IntConstant
| NullLiteral # Null
| StringLiteral # StringConstant
| $ # BooleanNonDeterministicChoice
| halt # HaltEvent
| this # SelfMachineReference
;
# Body of a tuple
tupleBody :
| rvalue ,
| rvalue (, rvalue)+
;
# Body of a named tuple
namedTupleBody:
| iden = rvalue ,
| iden = rvalue (, iden = rvalue)+
;
# r-value is an expression that can’t have a value assigned to it which
# means r-value can appear on right but not on left hand side of an assignment operator(=)
rvalue : expr ;
# rvalueList is a comma separated list of rvalue.
Primitives
P allows the common primitive expressions like literal-constants for integers, floats, strings, booleans, and the null value. There are three unique primitive expressions in P:
$
$ represents a nondeterministic boolean choice. It is a short hand for choose() which randomly returns a boolean value and the P Checker explores the behavior of the system for both the possibilities i.e., both when $ evaluates to true or false.
Halt
halt is a special event in P used for destroying an instance of a P machine. The semantics of an halt event is that whenever a P machine throws an unhandled event exception because of a halt event then the machine is automatically destroyed or halted and all events sent to that machine instance there after are equivalent to being dropped to ether. There are two ways of using the halt event: (1) self-halt by doing raise halt; raising a halt event which is not handled in the state machine will lead to that machine being halted or (2) by sending the halt event to a machine, and that machine on dequeueing halt, would halt itself. Please checkout the FailureDetector example in tutorials to know more about halt event
This
this represents the self machine reference of the current machine. It can be used to send self reference to other machines in the program so that they can send messages to this machine.
Formatted String
P allows creating formatted strings.
Syntax:: format ( formatString (, rvalueList)? )
formatString is the format string and rvalueList is a comma separated list of arguments for the formatted string.
var hw, h, w: string;
var tup: (string, int);
h = "Hello"; w = "World";
tup = ("tup value", 100);
hw = format("{0} {1}, and {2} is {3}!",
h, w, tup.0, tup.1);
// hw value is "Hello World, and tup value is 100!"
Formatted strings are most useful for printing logs. Checkout print statement.
var hw, h, w: string;
var tup: (string, int);
h = "Hello"; w = "World";
tup = ("tup value", 100);
print format("{0} {1}, and {2} is {3}!",
h, w, tup.0, tup.1);
// prints "Hello World, and tup value is 100!"
Tuple and Named Tuple Values
A tuple or named tuple value can be created using the following expressions:
Syntax (tuple value):: (rvalue ,) for a single field tuple value or (rvalue (, rvalue)+) for tuple with multiple fields.
// tuple value of type (int,)
(10,)
// tuple value of type (string, (string, string))
("Hello", ("World", "!"))
// assume x: int and y: string
// tuple value of type (int, string)
(x, y)
Syntax (named tuple value):: (iden = rvalue ,) for a single field named tuple value or (iden = rvalue (, iden = rvalue)+) for named tuple with multiple fields.
// named tuple value of type (reqId: int,)
(reqId = 10,)
// named tuple value of type (h: string, (w: string, a: string))
(h = "Hello", (w = "World", a = "!"))
// assume x: int and y: string
// named tuple value of type (a:int, b:string)
(a = x, b = y)
Access Field of Tuple and Named Tuple
The fields of a tuple can be
accessed by using the . operation followed by the field index.
Syntax (tuple value): expr.int where expr is the tuple value and int is the field index.
// tuple with three fields
var tupleEx: (int, bool, int);
tupleEx = (20, false, 21);
// accessing the first and third element of the tupleEx
tupleEx.0 = tupleEx.0 + tupleEx.2;
Named tuples are similar to tuples with each field having an associated name. The fields
of a named tuple can be accessed by using the . operation followed by the field name.
Syntax (named tuple value): expr.iden where expr is the named tuple value and iden is the field name.
// named tuple with three fields
var namedTupleEx: (x1: int, x2: bool, x3: int);
namedTupleEx = (x1 = 20, x2 = false, x3 = 21);
// accessing the first and third element of the namedTupleEx
namedTupleEx.x1 = namedTupleEx.x1 + namedTupleEx.x3;
Indexing into a Collection
P supports three collection types: map, seq, and set. We can index into these collection types to access its elements.
Syntax: expr_c[expr_i]
If expr_c is a value of sequence type then expr_i must be an integer expression and expr_c[expr_i] represents the element at index expr_i. Similarly, If expr_c is a value of set type then expr_i must be an integer expression and expr_c[expr_i] represents the element at index expr_i but note that for a set there is no guarantee for the order in which elements are stored in the set.
Finally, if expr_c is a value of map type then expr_i represents the key to look up and expr_c[expr_i] represents the value for the key expr_i.
Operations on Collections
P supports four other operations on collection types:
sizeof
Syntax:: sizeof(expr), where expr is a value of type set, seq or map, returns an integer value representing the size or length of the collection.
var sq: seq[int];
while (i < sizeof(sq)) {
...
i = i + 1;
}
keys and values
Programmers can use keys and values functions to get access to a sequence of all the keys or values in map respectively.
Syntax:: keys(expr) or values(expr)
expr must be a map value, if expr : map[K, V] then keys(expr) returns a sequence of all keys in the map (of type seq[K]) and similarly, values(expr) returns a sequence of all values in the map (of type seq[V]).
Primarily, keys and values are used to get contents of the map and then operate over it.
contains (or in)
To check if an element (or key in the case of a map) belongs to a collection, P provides the in operation.
Syntax: expr_e in expr_c
expr_e is the element (or key in the case of map) and expr_c is the collection value. The in expression evaluates to true if the element belongs to the collection and false otherwise.
var sq: seq[tRequest];
var mp: map[int, tRequest];
var rr: tRequest; var i: int;
...
if(rr in sq && rr in values(mp) && i in mp) { ... }
Default value for a type
The default primitive in P can be used to obtain the default value for any type.
Syntax: default(type)
type is any P type and default(type) represents the default value for the type. The default values for all P types is provided here.
New
New expression is used to create an instance of a machine, new returns a machine reference to the newly created instance of the machine.
Syntax: new iden (rvalue?) ;
iden is the name of the machine to be created and rvalue is the optional constructor parameter that becomes the input parameter of the entry function of the start state of the machine.
new Client((id = 1, server = this));
(id = 1, server = this)
which is delivered as a payload to the entry function of the start state of the created Client machine.
Function Call
Function calls in P are similar to any other imperative programming languages.
Note that the parameters passed to the functions and the return values are pass-by-value!
Syntax: iden ( rvalueList? ) ;
iden is the name of the function and rvalueList is the comma separated list of function arguments.
x = Foo();
y = Bar(10, "haha");
Negation and Not
P supports two unary operations: - on integers and floats values (i.e., negation) and ! on boolean values (i.e., logical not).
Arithmetic
P supports the following arithmetic binary operations on integers or floats: + (i.e., addition), - (i.e., subtraction), * (i.e., multiplication), % (i.e., modulo), and / (i.e., division).
Comparison
P supports the following comparison binary operations on integers or floats: < (i.e., less-than), <= (i.e., less-than-equal), > (i.e., greater-than), and >= (i.e., greater-than-equal).
Cast
P supports two super types any and data (more details). To cast values from these supertypes to the actual types, P supports the as cast expression.
Syntax: expr as T
expr expression is cast to type T and if the cast is not valid then it leads to dynamic type-cast error.
type tRecord = (key: int, val: any);
...
var st: set[tRecord];
var x: any;
var x_i: string;
var st_i: set[(key: int, val: string)];
x_i = x as string;
st += ((key = 1, val = "hello"));
st_i = st as set[(key: int, val: string)];
...
Coerce
P supports coercing of any value of type float to int and also any enum element to int.
Syntax: expr to T
expr expression is coerced to type T. We currently support only coercing of type float to int and also any enum element to int.
enum Status {
ERROR = 101,
SUCCESS = 102
}
...
var x_f : float;
var x_i: int;
x_f = 101.0;
x_i = x_f to int;
assert x_i == ERROR to int;
Choose
P provides the choose primitive to model data nondeterminism in P programs. The P checker then explores the behavior of the program for all possible values that can be returned by the choose operation.
Syntax: choose() or choose(expr)
expr can either be a int value or a collection. For choose(x), when x is an integer, choose(x) returns a random value between 0 to x (excluding x), when x is a collection then choose(x) returns a random element from the collection.
choose() // returns true or false, is equivalent to $
choose(10) // returns an integer x, 0 <= x < 10
choose(x) // if x is set or seq then returns a value from that collection
The choose operation can be used to model nondeterministic environment machines that generate random inputs for the system. Another use case could be to model nondeterministic behavior within the system itself where the system can randomly choose to timeout or fail or drop messages.
Performing a choose over an empty collection leads to an error. Also, choose from a map value returns a random key from the map.
Note that the maximum number of choices allowed in a choose(expr) is 10,000. Performing a choose with an int value greater than 10000 or over a collection with more than 10000 elements leads to an error.
choose(10001) // throws a compile-time error
choose(x) // throws a runtime error if x is of integer type and has value greater than 10000
choose(x) // throws a runtime error if x is of seq/set/map type and has size greater than 10000 elements