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)
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)
...