Random numbers and counters

The functional module RANDOM adds to NAT a pseudo-random number generator:

  fmod RANDOM is
    protecting NAT .
    op random : Nat -> Nat [special (...)] .
  endfm

The function random is the mapping from Nat into the range of natural numbers $[0, 2^{32}-1]$ computed by successive calls to the Mersenne Twister Random Number Generator.^7.3For example,

  Maude> red in RANDOM : random(17) .
  result NzNat: 1171049868

Although random is purely functional, it caches the state of the random number generator so that evaluating random(0) is always fast, as is evaluating random(n+1) if random(n) was the previous call to the operator random. In general, after generating random(n), both random(n) and random(n+1) are computed efficiently because random(n) is a look up, while random(n+k) takes k steps of the twister or O(k) time.

By default the seed 0 is used, but a different seed, giving rise to a different function, may be specified by the command line option -random-seed=$n$, where $n$ is a natural number in the range $[0, 2^{32}-1]$. For example, if we invoke the Maude interpreter with the option -random-seed=42 and run the previous example again we get

  Maude> red in RANDOM : random(17) .
  result NzNat: 613608295

The predefined system module COUNTER adds a ``counter'' that can be used to generate new names and new random numbers in Maude programs that do not want to explicitly maintain this state.

  mod COUNTER is
    protecting NAT .
    op counter : -> [Nat] [special (...)] .
  endm

For the rewrite and frewrite commands (see Sections 5.4 and 16.2), as well as the erewrite command (see later Section 8.4), the built-in constant counter has special rule rewriting semantics: each time it has the opportunity to do a rule rewrite, it rewrites to the next natural number, starting at 0. In this way the predefined system module COUNTER provides a built-in strategy for the application of the implicit nondeterministic rewrite rule

  rl counter => N:Nat .

that rewrites the constant counter to a natural number. The built-in strategy applies this rule so that the natural number obtained after applying the rule is exactly the successor of the value obtained in the preceding rule application.

We can use the COUNTER module together with the predefined RANDOM module described above to sample various probability distributions. We illustrate the general idea with the following SAMPLER module, which can be used to sample a Bernoulli distribution corresponding to tossing a biased coin. This module also imports the predefined module CONVERSION, described later in Section 7.9, which includes conversion functions between different types of numbers.

  mod SAMPLER is
    pr RANDOM .
    pr COUNTER .
    pr CONVERSION .
    op rand : -> [Float] .
    op sampleBernoulli : Float -> [Bool] .
    rl rand => float(random(counter) / 4294967295) .
    rl sampleBernoulli(P:Float) => rand < P:Float .
  endm

The first rule rewrites the constant rand to a floating point number between $0$ and $1$ pseudo-randomly chosen according to the uniform distribution. This floating point number is obtained by converting the rational number random(counter) / 4294967295 into a floating point number, where 4294967295$= 2^{32}-1$ is the maximum value that the random function can attain. We can then use the uniform sampling of a number between $0$ and $1$ to sample the tossing of a coin with a given bias P:Float between $0$ and $1$. This is accomplished by the second rewrite rule in SAMPLER.

Sampling capabilities defined in this style for different probability distributions can then be used to specify probabilistic models in Maude. We can give a flavor for how such models can be simulated in Maude by means of a simple battery-operated clock example. We may represent the state of such a clock as a term clock(T,C), with T a natural number denoting the time, and C a positive real denoting the amount of battery charge. Each time the clock ticks, the time is increased by one unit, and the battery charge slightly decreases; however, the lower the battery charge, the greater the chance that the clock will stop, going into a state of the form broken(T,C). We can model this system by means of the following Maude specification:

  mod CLOCK is
    pr SAMPLER .
    sort Clock .
    op clock : Nat Float -> Clock [ctor] .
    op broken : Nat Float -> Clock [ctor] .
    var T : Nat .
    var C : Float .
    rl clock(T,C) 
      => if sampleBernoulli(C / 1000.0)
         then clock(s(T), C - (C / 1000.0))
         else broken(T, C) 
         fi .
  endm

This rule models the fact that each time the clock is going to tick a coin is tossed; if the result is true, then the clock ticks normally, but if the result is false, then the clock breaks down. If the battery charge is high enough, the bias of the coin will be highly towards normal ticking, but as the battery charge decreases, the bias gradually decreases, so that a breakdown becomes increasingly likely.

One can use a module such as CLOCK above to perform Monte Carlo simulations of the probabilistic system we are interested in. Of course, we want different arguments for the random number generator to be used each time from the same initial state so that we obtain different behaviors. In Maude this can be easily achieved within the same Maude session by typing the command

  set clear rules off .

which turns off the automatic clearing of rule state information, including counter values (see Section 16.2). This means that when we run several times the same computation, a different counter value will be initially used each time, therefore getting different behaviors in the expected Monte Carlo way. For example, we get the following simulations for the behavior of a clock until it breaks:

  Maude> rewrite in CLOCK : clock(0, 1.0e+3) .
  result Clock: broken(40, 9.607702107358117e+2)

  Maude> rewrite in CLOCK : clock(0, 1.0e+3) .
  result Clock: broken(46, 9.5501998182355942e+2)

  Maude> rewrite in CLOCK : clock(0, 1.0e+3) .
  result Clock: broken(16, 9.8411944181564002e+2)

  Maude> rewrite in CLOCK : clock(0, 1.0e+3) .
  result Clock: broken(6, 9.9401498001499397e+2)

  Maude> rewrite in CLOCK : clock(0, 1.0e+3) .
  result Clock: broken(28, 9.7237474437709557e+2)

Since it is reasonable for a program to use multiple counters, the safe way to do this is to import renamed copies of COUNTER; for example

  protecting COUNTER * (op counter to counter2) .

Counters are inactive with respect to search, model checking, and equational rewriting. Notice that there are potentially bad interactions with the debugger (see Section 13.1.3) since another rewrite/frewrite/erewrite executed in the debugger will lose the counter state of the interrupted rewrite/frewrite/erewrite.