Mora - Automatic Generation of Moment-Based Invariants
495
Fig. 3. MORA workflow diagram.
In the rest of the paper, we will illustrate the main steps of MORA, by considering
Figure 1 as its input loop and [1, 2] as its list of input goals. With such an input
goal, MORA is set to compute the first and second moments of each variable of Figure 1. Note, that even if 1 was omitted from the aforementioned input goal, MORA
would still need to compute some of the first moments of the variables, as they are
required for computing the second-order moments. In the sequel, we show-case the
MORA behaviour for:
mora("running", [1, 2]).
(1)
4 MORA– Tool Overview
We first give details on our implementation. We then present the overall workflow of
MORA in Figure 3, based on which we overview the main components of our tool.
Overall Implementation. MORA is implemented in python3, requiring python
version of at least 3.7. MORA relies on the diofant and scipy libraries: (i) the
python library diofant is used in MORA for symbolic mathematical computations
and recurrence solving; (ii) the scipy library, and in particular its statistics module
scipy.stats, is used in MORA to handle probability distributions and statistical
functions, as well as to simplify and compute expressions involving probability distributions and initial values of variables. Altogether, our implementation comprises of
around 350 lines of code.
MORA – Parser. MORA first checks whether a given input program is Prob-solvable,
by checking the requirements of Section 2. If the input program is not Prob-solvable, an
error is reported, and the execution of MORA stops. Otherwise, within its parser module,
MORA extracts initial values from its input loop, rewrites loop updates into equations
over expected values of monomial expressions over loop variables, and processes the
list of its input goals to identify which higher-order moments need to be computed.
For our demo execution (1), MORA extracts the initial value x(0)=0, where x(0)
denotes the initial value of x before the loop. Using the input goals specified in (1),
MORA is set to compute the expected values of {u, g, x, y, uˆ2, gˆ2, xˆ2,
495
Fig. 3. MORA workflow diagram.
In the rest of the paper, we will illustrate the main steps of MORA, by considering
Figure 1 as its input loop and [1, 2] as its list of input goals. With such an input
goal, MORA is set to compute the first and second moments of each variable of Figure 1. Note, that even if 1 was omitted from the aforementioned input goal, MORA
would still need to compute some of the first moments of the variables, as they are
required for computing the second-order moments. In the sequel, we show-case the
MORA behaviour for:
mora("running", [1, 2]).
(1)
4 MORA– Tool Overview
We first give details on our implementation. We then present the overall workflow of
MORA in Figure 3, based on which we overview the main components of our tool.
Overall Implementation. MORA is implemented in python3, requiring python
version of at least 3.7. MORA relies on the diofant and scipy libraries: (i) the
python library diofant is used in MORA for symbolic mathematical computations
and recurrence solving; (ii) the scipy library, and in particular its statistics module
scipy.stats, is used in MORA to handle probability distributions and statistical
functions, as well as to simplify and compute expressions involving probability distributions and initial values of variables. Altogether, our implementation comprises of
around 350 lines of code.
MORA – Parser. MORA first checks whether a given input program is Prob-solvable,
by checking the requirements of Section 2. If the input program is not Prob-solvable, an
error is reported, and the execution of MORA stops. Otherwise, within its parser module,
MORA extracts initial values from its input loop, rewrites loop updates into equations
over expected values of monomial expressions over loop variables, and processes the
list of its input goals to identify which higher-order moments need to be computed.
For our demo execution (1), MORA extracts the initial value x(0)=0, where x(0)
denotes the initial value of x before the loop. Using the input goals specified in (1),
MORA is set to compute the expected values of {u, g, x, y, uˆ2, gˆ2, xˆ2,