Basic tutorial

Note

This page contains a set of examples to show the basic usage of NuZot. All the examples are saved in the examples folder. You can either type them in the shell manually or simply load the file.

To open the shell run java -jar NuZot.jar --shell.

Using SMT-lib instructions

The example GreaterThan.zot shows how to run SMT-like coommands in NuZot. Open the shell and type:

(set-info :k 5)
(declare-fun x () Int)
(assert (> x 5))
(get-model)

Which means that in a time from 0 to 5 the property x > 5 has to be satisfied. NuZot verify the property and creates the model:

Model:
loopex -> true
iLoop -> 4
x -> 6
zot-p0 -> {
  1 -> true
  6 -> true
  0 -> true
  2 -> true
  3 -> true
  4 -> true
  5 -> true
  else -> true
}
(get-model)

You can run the push and pop example by executing java -jar NuZot.jar --file examples/GreaterThan.zot.

Push and Pop example

NuZot supports a push and pop interface. To save the status of your model use the (push) command. To restore the last stored state use the (pop) command.

Open the NuZot shell and type:

(set-info :k 5)
(declare-fun x () Int)
(push)
(assert (= x 5))
(get-model)
(pop)
(assert (= x 10))
(get-model)

NuZot will produce the following output. Notice that after the pop the model is discarded and recreated.

Welcome to NuZot shell.
Type '(exit)' to leave.
Type '(save "filename")' to save.
Type '(load "filename")' to load a script at the current stack level.
NuZot>(set-info :k 5)
(set-info :k 5)
NuZot>(declare-fun x () Int)
(declare-fun iLoop () Int)
(declare-fun loopex () Bool)
(assert (or (! loopex) (and (< 0 iLoop) (<= iLoop 5))))
(declare-fun x () Int)
NuZot>(push)
(push)
Stack level: 2
NuZot>(assert (= x 5))
(declare-fun zot-p0 (Int) Bool)
(assert (zot-p0 1))
(assert (-> loopex (iff (zot-p0 6) (zot-p0 iLoop))))
(assert (-> (! loopex) (! (zot-p0 6))))
(assert (iff (zot-p0 0) (= x 5)))
(assert (iff (zot-p0 1) (= x 5)))
(assert (iff (zot-p0 2) (= x 5)))
(assert (iff (zot-p0 3) (= x 5)))
(assert (iff (zot-p0 4) (= x 5)))
(assert (iff (zot-p0 5) (= x 5)))
(assert (iff (zot-p0 6) (= x 5)))
NuZot>(get-model)
(get-model)
Model:
loopex -> true
iLoop -> 4
x -> 5
zot-p0 -> {
  1 -> true
  6 -> true
  0 -> true
  2 -> true
  3 -> true
  4 -> true
  5 -> true
  else -> true
}

NuZot>(pop)
(pop)
Stack level: 1
NuZot>(assert (= x 10))
(declare-fun zot-p1 (Int) Bool)
(assert (zot-p1 1))
(assert (-> loopex (iff (zot-p1 6) (zot-p1 iLoop))))
(assert (-> (! loopex) (! (zot-p1 6))))
(assert (iff (zot-p1 0) (= x 10)))
(assert (iff (zot-p1 1) (= x 10)))
(assert (iff (zot-p1 2) (= x 10)))
(assert (iff (zot-p1 3) (= x 10)))
(assert (iff (zot-p1 4) (= x 10)))
(assert (iff (zot-p1 5) (= x 10)))
(assert (iff (zot-p1 6) (= x 10)))
NuZot>(get-model)
(get-model)
Model:
loopex -> true
iLoop -> 5
x -> 10
zot-p1 -> {
  1 -> true
  6 -> true
  0 -> true
  2 -> true
  3 -> true
  4 -> true
  5 -> true
  else -> true
}

NuZot>(exit)
(exit)
NuZot shell terminated

You can run the push and pop example by executing java -jar NuZot.jar --file examples/PushAndPop.zot.

Using LTL instructions

The example OnlyTomorrow.zot shows a predicate which is only satisfied for one instant:

(set-info :k 5)
(declare-tfun x () Bool)
(assert (! x))
(assert (next x))
(assert (! (next (next x))))
(get-model)

If you run this example by executing java -jar NuZot.jar --file examples/OnlyTomorrow.zot.

NuZot will generate the following model:

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

Advanced tutorial

Please continue to the advanced tutorial page.