Advanced tutorial

Notes

This page describes advanced features which have been embedded in NuZot. Before reading this page please be sure that you have understood how NuZot work. We strongly encourage you to read the basic tutorial page.

Using Real instead of integers

Normally NuZot would work with boolean and integers. It is possible to use reals instead of integers but there are few limitations:

• Integers and real cannot be mixed. You can use either booleans and integers or booleans and reals.
• At the time of this release real support is limited by Z3. Z3 hallows to define a real sort but does not let you specify floating point variables. NuZot internally converts floating point numbers as fractions with a limited precision. Using this trick it is possible to use reals with Z3. For instance 0.55 is converted in 55/100. Notice that a value like 1e-20 is converted in 0.
• Using the division of two integers to simulate a real STRONGLY reduce the precision of the result.

Specifying the domain

The initialization command (set-info :domain Int) sets the integer domain. This is active by default. The command (set-info :domain Real) sets the real domain.

The UsingReals.zot example shows how you can use reals in your scripts. From the command line run java -jar NuZot.jar --file examples/UsingReals.zot. This will execute the following code:

(set-info :domain Real)
(set-info :k 5.0)
(declare-fun x () Real)
(assert (next (> x 0.12)))
(check-sat)
(get-model)

For this script NuZot will generate the following model. Please notice that the value of x is expressed as a fraction and not as a floating point.

Model:
loopex -> true
iLoop -> 1
x -> 28/25
zot-p0 -> {
  1 -> true
  6 -> false
  1 -> false
  0 -> true
  2 -> true
  3 -> true
  4 -> true
  5 -> true
  else -> true
}
zot-p1 -> {
  6 -> true
  1 -> true
  0 -> true
  1 -> true
  2 -> true
  3 -> true
  4 -> true
  5 -> true
  else -> true
}

Using a different logic

NuZot allows developers to define their own temporal expansion and to use it at run-time. This feature is mainly for research and development purposes. We call them interpreter delegates.

The runtime loading uses java/scala reflection. The desired interpreter delegate is loaded by class name in the init script and used for the rest of the computation. Once selected those delegates cannot be replaced.

How does the LTLInterpreter works

The scala trait trait DSLInterpreterDelegate defines a delegate which interpreter can use depending on their implementation. The LTLInterperter when expanding temporal formulas can use a set of three delegates:

• An instance of trait ArithmeticDelegate extends DSLInterpreterDelegate which will be in charge of performing the temporal expansion of arithmetic operators (such as (+ x y)).
• An instance of trait EqualityDelegate extends DSLInterpreterDelegate which will do the temporal expansion of equalities and inequalities (i.e. (> x y)).
• An instance of trait LogicDelegate extends DSLInterpreterDelegate which will perform the temporal expansion of logic formulas.

Developers can implement their own delegates and expand the temporal logic as their desire by extending from one of those trait. Note implementing multiple trait is not a good idea and can lead to side effects.

Specifying delegates at run-time

A script can specify a delegate by specifying it in the init command, for example (set-logic bar.foo.MyDelegate). During the initialization all the given delegates are loaded by class name and they are assigned according to their type.

Running java -jar NuZot.jar --file examples/Delegates.zot will show you an example in which we have redefined at run-time the default delegates.

(set-logic it.polimi.nuzot.ltl.DefaultEqualityDelegate)
(set-logic it.polimi.nuzot.ltl.FOArithmeticDelegate)
(set-logic it.polimi.nuzot.ltl.LTLLogicDelegate)
(set-info :k 10.0)
(set-info :domain Real)
(declare-tfun x () Real)
(assert (next (= x 0.1)))
(check-sat)
(get-model)