2.1.2.1 Algorithm for generating connected graphs

lbtt uses the following algorithm for generating random connected graphs:

     1  function RandomGraph(n : Integer; d : Real in [0.0,1.0];
                             t : Real in [0.0,1.0]) : Graph;
     2      S := {s1, s2, ..., sn};
     3      NodesToProcess := {s1};
     4      UnreachableNodes := {s2, s3, ..., sn};
     5      Edges := {};
     6      while NodesToProcess is not empty do begin
     7          state := a random node in NodesToProcess;
     8          remove state from NodesToProcess;
     9          Label(state) := {};
     10         for all p in AP do
     11             if RandomNumber(0.0, 1.0) < t then
     12                 insert p into Label(state);
     13         if UnreachableNodes is not empty then begin
     14             state' := a random node in UnreachableNodes;
     15             remove state' from UnreachableNodes;
     16             insert state' into NodesToProcess;
     17             insert (state,state') into Edges;
     18         end;
     19         for all state' in S do
     20             if RandomNumber(0.0, 1.0) < d then begin
     21                 insert (state,state') into Edges;
     22                 if state' is in UnreachableNodes then begin
     23                     remove state' from UnreachableNodes;
     24                     insert state' into NodesToProcess;
     25                 end;
     26             end;
     27         if there is no edge (state,state') in Edges
                                          for any state' in S then
     28             insert (state,state) into Edges;
     29     end;
     30     return <S, Edges, s1, Label>;
     31 end;

The algorithm receives the parameters n (number of states in the state spaces), d (approximate density of the generated graph) and t (the probability with which each of the propositions in AP should hold in a state) and returns the generated state space as a quadruple <S, Edges, s1, Label>. Here S is the set of states, Edges is the set of directed edges between the states, s1 is a state from which every state of the state space can be reached, and Label is a function which maps each state to its label (a subset of AP).