RVS: Examples of properties to check

Rules from Baralis' paper

The rules

See baralis-rules.ilr.

The checks

The bad_account, raise_rate, SF_bonus, and decrease_bad rules have conditions on the rate attribute of an account, and/or modify this attribute. The following checks can be envisionned:

• Check that there is no ambiguity between this rules, that is, there is no value of the rate that could cause more than one rule to be applicable. Or the action parts of these rules are not contradictory (the rules are confluent).
• Check that all rules are useful, that is, there is no rule that will never be matched because no rate value would cause its LHS to evaluate to true. This could be intrinsic to the rule, eg. (rate < 1 && rate > 2). Or this could come from the fact that, knowing the initial value of an account's rate, the rate value after applying the possible rules can never fall into the range matched by some rule. This would require the user to specify the initial value of an account's rate. Or this could result into a constraint on the allowed initial value of an account's rate.
• Check that, since the rate is used both in the LHS and in the RHS of rules, this set of rules always terminates. If not, determine for which initial value of an account's rate there are loops, and due to which rules.

Extension

Suppose we add the following rule:

// Rule remove-empty-bad cleans the LOW-ACC relation by removing 0-day periods.

rule remove_empty_bad {
  when {
    low: LowAcc(start equals end);
  } then {
    remove low;
  }
}

Suppose also that the start_bad rule has a typo, and the first condition reads 'Account(n: num; balance <= 500)'. Then if an account has a balance of exactly 500, then the engine would loop, creating and removing 0-day periods.

The user may want a check against this kind of problems.

Car allocation (example from the training)

The rules

See car-allocation.ilr (the car-allocation.irl file contains the ruleset as exported from the Builder).

The checks

The ruleflow itself is purely linear. So there's nothing much to check on it.

A possible check could be a precondition of task basic_assignment stating that all cars in working memory are present.

A check for the whole ruleset can be that the reservation attribute of cars is not set more than once; and similarly, that the car attribute of reservations is not set more than once, except by rule exception.bumped_upgrade. This would require the user to explicit the semantics of the Reservation.isAssigned() and the Car.reserved() methods, with respect to the two attributes.

A postcondition of task free_upgrade could be to verify that frequent customers get better upgrades than non-frequent customers. One could propose to modify the free_upgrade.free_upgrade_loyalty_program rule's priority to be 'customer.nbRentals + 1'. The check could then be worded as: considering to reservations upgraded from the same requested group, the customer with the highest group has more rentals than the other.

I don't fully understand the exception.bumped_upgrade rule.