Integer value:

int(Nr)

where Nr is an integer

Booleans:

pred_true pred_false

Enumerated or deferred set elements:

fd(Nr,Type)

where Nr is an integer >= 1 and Type is an atom representing the type of enumerated/deferred set

Strings

string(S)

where S is an atom

Pairs/couples

(Val1,Val2)

where Val1 and Val2 are values

Records

rec(Fields)

where Fields is a list of terms:

field(Name,Val)

where Name is atom representing the field name and Val is a value.

The fields are sorted by name!

Sets Here is an overview of the set representations:

[] [Val|Set] avl_set(AVL) closure(P,T,B) global_set(GS) freetype(T)

The empty set is encoded as the empty list.

[]

This represents a set containing at least the value Val and the rest:

[Val|Set]

Note that Set can in principle be any other form (e.g., avl_set(.)).
The predicate `expand_custom_set_to_list` can be used to transform a set into a form using only the empty list and the `[.|.]` functor.

The next are called custom explicit sets, they always represent a fully known set.

A set can be represented by a non-empty AVL tree:

avl_set(AVL)

Given a list of parameter identifiers, a list of types and a predicate AST B, we can represent the set {P| P:T & B} as follows:

closure(P,T,B)

There are custom representations for complete types, these may be phased out in the future and replaced by the closure(.,.,.) representation:

global_set(GS) freetype(T)

Freetype values

freeval(Id,Case,Value)

Constructor for denoting special values (undefined values, experimental support for reals,..)

term(Term)

`term(undefined)` is used for uninitialised variables (e.g., when using the B `VAR` construct).
`term(floating(Nr)` is currently used for floating numbers, but this will probably change in the future.

An AST node has the form:

b(Expr,Type,Infos)

Expr generally has the form Functor(AST1,...,ASTk). Below we list possible cases.
The predicate `syntaxelement` in bsyntaxtree.pl lists all allowed forms of Expr.
Type is either `pred` for predicates, `subst` for substitutions or the value type for expressions, see below.
Infos contains information about the AST node and is explained next.

Infos should be a ground list of informations. Some important information fields are:

contains_wd_condition used_ids(Ids) nodeid(PositionInfo) refers_to_old_state(References)

Possible types are:

pred subst integer real boolean string global(G) couple(Type1,Type2) record(FieldTypes) set(Type) seq(Type) freetype(F)

where FieldTypes is a list containing:

field(Name,Type)

The `real` type has been added in version 1.10 of ProB.

boolean_false boolean_true bool_set

...

card(AST) domain(AST) front(AST)

...

cartesian_product(AST1,AST2) composition(AST1,AST2) concat(AST1,AST2) conjunct(AST1,AST2)

...

general_sum(Ids,AST,AST) general_product(Ids,AST,AST) lambda(Ids,AST,AST) quantified_union(Ids,AST,AST) quantified_intersection(Ids,AST,AST) set_extension(ListOfASTs) sequence_extension(ListOfASTs)

...