• CMPE 278 2007 HW 5

In this homework, you will specify and verify some properties of the traffic light example.

Specification

Defining sets of states

Note that via the stateset directive, you can create named sets of states, as described in the Ticc input grammar. You can do it in two ways:

• At the local level, inside a module, you can write:

  stateset id: exp
  

  or, for instance,

  stateset light_is_red : (l = 1) | (l = 2)
  

  The advantage of this is that your stateset can cite variables that are local to a module.

• At the global level, outside of all modules, you can use the same syntax:

  stateset id: exp
  

  but this time, you cannot cite local variables.

Note that stateset declarations must follow the declaration of the variables to which they refer.

Once this is done, you can construct mdds corresponding to these statesets as follows:

• Local: b = get_stateset symb_module_name stateset_name puts in b the mdd for the corresponding stateset. Note that stateset_name is the name of a symbolic module (the name on the left hand side of mk_sym.

• Global: b = mk_set stateset_name puts in b the mdd for the corresponding stateset.

You can also parse sets of states directly using parse_stateset. You can get the set of initial states of a module via get_initial. See ticc.mli for more information.

Combining sets of states

You can form boolean combinations of sets of states using the functions set_and set_or set_impl set_not, and you can test for emptiness via set_is_empty set_is_nonempty set_equal set_is_subset. Again, see ticc.mli.

Evaluating CTL formulas

You can evaluate CTL formulas via the following functions (remember: F is used in place of <> and G is used in place of [] as alternative notation):

• ctl_e_f : E<> operator

• ctl_e_g : E[] operator

• ctl_a_f : A<> operator

• ctl_a_g : A[] operator

Specification

Given the above tools, you now have all the instruments to specify, and verify, properties of your traffic light example. Specify, and verify, the following properties. Properties denoted with must hold; properties not denoted by may or may not hold for your implementation, and you need to say if they do. Let's focus on properties not involving turn signals.

• Every traffic light can eventually turn green from the initial state.

• No traffic light can get stuck in a situation in which it will never be able to change color again.

• If two lights are in 90 degrees directions one from the other, then if one is yellow or green, the other one must be red.

• Whenever some car requests to pass, it is always the case that the light turns green at some point later in the future.

• Whenever some car requests to pass, it is not the case that the light stays surely red forever.