Code Execution

For instance, the following scenario counts the number of proposals of round 1 until level 10:

#![allow(unused)]
fn main() {
let cpt = ref 0

let scenario_code =
  (add_spec ~post:[ Exec (fun _ -> incr cpt; return_unit) ] @@
   proposal __ __ (round 1) __ [__]
   ) || any_step 
   ->? proposal __ (level 10) __ __ [__]
}

The scenario is composed of a single loop which waits for a proposal of level 10. In the body of the loop, we accept proposals of round 1 or any other step, but we have added a post-condition to the step proposal which increments a counter.

At the end of the execution, the variable cpt will contain the number of proposal messages at round 1 that the proxy has seen go through.

Another use of Exec is to perform queries or actions on the node, such as injecting operations to specific nodes:

#![allow(unused)]
fn main() {
Exec (Helpers.inject_dummy (N "b1"))
}

Injects a dummy transaction of 1 mutez from b1 to itself, onto the node b1.