SKEDSOFT

BED Commands for SimpleTR:: The BED commands given in Figure 11.5 compute the reachable set of states using forward reachability in our example. We can see that P2, the least fixed-point, is indeed true — namely, the characteristic predicate for the set of all states. (Note: In BED, the primed variables must be declared immediately after the unprimed counterparts). In addition to the explicit commands to calculate the least fixed-point, BED also provides a single command called reach. Using that, one can calculate the least fixed-point in one step. In our present example, RS and P2 end up denoting the BDD for true.

let RS = reach(I,T)
upall RS
view RS
Section 11.3.4 discusses another example where the details of the fixedpoint iteration using BED are discussed.

Fig. 11.5. BED commands for reachability analysis on SimpleTR, and the
fixed-point iteration leading up to the least fixed-point that denotes the set
of reachable states starting from I