merc_syntax 2.0.0

Provides an AST and Pest grammar for the mCRL2 specification language.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23

map @func_update: (S -> T) # S # T -> (S -> T);
    @func_update_stable: (S -> T) # S # T -> (S -> T);
    @is_not_an_update: (S->T) -> Bool;
% The function below evaluates a condition, and if it is not true, else is always chosen. 
    @if_always_else: Bool # (S -> T) # (S -> T) -> (S -> T);

var x: S;
    y: S;
    v: T;
    w: T;
    f: S -> T;

% The first rule below should only be applied if f is not preceded by a @func_update_stable, or a @func_update. 
eqn  @is_not_an_update(f) -> @func_update(f,x,v) = @if_always_else(f(x) == v,f,@func_update_stable(f,x,v));
     @func_update(@func_update_stable(f,x,w),x,v) = @if_always_else(f(x) == v,f,@func_update_stable(f,x,v));
     y < x -> @func_update(@func_update_stable(f,y,w), x,v) = @func_update_stable(@func_update(f,x,v),y,w);
     x < y -> @func_update(@func_update_stable(f,y,w), x,v) = 
                     @if_always_else(f(x) == v,
                                     @func_update_stable(f,y,w),
                                     @func_update_stable(@func_update_stable(f,y,w), x,v));
     x != y -> @func_update_stable(f,x,v)(y) = f(y);
     @func_update_stable(f,x,v)(x) = v;
     @func_update(f,x,v)(y) = if(x == y,v,f(y));