DEFINITIONS
 // external functions and predicates that serve as annotations for ProB
 
 EXTERNAL_FUNCTION_FORCE(T) == T --> T;
 FORCE(value) == value;
 // forces evaluation of symbolic set representations
 // usage FORCE( { x | x:1..100 & x mod 2 = 0 } )
 
 EXTERNAL_PREDICATE_ENUMERATE(T) == T;
 ENUMERATE(identifier) == (1=1);
 // usage ENUMERATE(y) & x:1..2 & y:200..300 & x = y mod 3  --> will generate y=200,x=2 first
 
 EXTERNAL_PREDICATE_DO_NOT_ENUMERATE(T) == T;
 DO_NOT_ENUMERATE(identifier) == (1=1);
 
 EXTERNAL_FUNCTION_COPY(T) == T --> T;
 COPY(value_to_copy)==value_to_copy;
 // can be used as an "enumeration barrier"; value is copied only once it is fully known

 EXTERNAL_PREDICATE_ASSERT_TRUE == BOOL*STRING;
 ASSERT_TRUE(assert_bool_expr,str) == (1=1);
 // usage ASSERT_TRUE(bool(Pred),"Error Message")
 
 EXTERNAL_FUNCTION_ASSERT_EXPR(T) == BOOL*STRING*T --> T;
 ASSERT_EXPR(assert_bool_expr,str,v) == v;
