Implement visualize with Before/After predicate in Execute by Predicate when no solution is found

One can also define the values of variables after executing the INITIALISATION or an operation. In this case, the contradiction cannot be found in the guard when no solution is found.

In the following example, one can define a predicate such as "z = 2 & y = 4". The guard is true but there is no succeeding state such that "y = 4" is true. Solving this issue require implementing a Before/After predicate.