Chapter 1: Fundamental

1.2 Finding Strings

In this section, you will learn how to use Cyclone to find all possible strings with a particular length from a given DFA (deterministic finite automaton). DFA is a state machine and essentially is a graph. So it can be described by Cyclone.

For example, the following DFA describes a machine M that accepts strings that start and end with the same symbol.

This example is taken from Introduction to the Theory of Computation (3rd Edition), Page 38, Example 1.11

The states (q1 and r1) with double circles indicate they are accepting states or final states of M.

Suppose we wish to find all possible strings with a length of 5. We now can write a Cyclone specification for this machine M.

The specification is shown below:

  machine M {

      abstract start state  S{}

      abstract final state  q1{}

      abstract state q2{}

      abstract final state  r1{}

      abstract state r2{}

      trans  t1 { S->q1  on "a" }

      trans  t2 { S->r1  on "b" }

      trans  t3 { q1->q1  on "a" }

      trans  t4 { q1->q2  on "b" }

      trans  t5 { q2->q1  on "a" }

      trans  t6 { q2->q2  on "b" }

      trans  t7 { r1->r1  on "b" }

      trans  t8 { r1->r2  on "a" }

      trans  t9 { r2->r1  on "b" }

      trans  t10 { r2->r2  on "a" }

/*

       * Goal: find all strings with length of 5.

*/

     goal{

         enumerate for 5

Some of the keywords in Cyclone are interchangeable. Since we are talking about a DFA machine here, it will make much more sense to consider a node in a graph as a state. Hence, we use keywords state and trans instead of node and edge used in previous Section. The keywords state and node here are interchangeable, the same for edge and trans. In this context, they have the same semantics that is creating nodes and edges in a graph. Similarly, we also change graph to machine. By using these keywords, it makes our DFA specification more meaningful in a specific context, particularly when we share it with others. Here is a list of keywords are interchangeable in Cyclone.

The keyword final here defines a state (node) to be a stopping state or terminating point. In a Cyclone specification, one can define multiple final states but with exactly one start state. The keyword on allows us to label a transition (edge) with a string.

The enumerate in goal section asks Cyclone to find all possible paths from a defined starting state (node) to one of the final states (nodes). In previous Section, we used reach statement to check if a node is reachable. Here, we didn't use it since the states q1 and r1 are already defined as final states. Both condition (introduced in previous Section) and reach statements are optional for a goal. However, if you have no final states in your machine (graph), then you must supply a reach statement in your goal.

Say, you use a reach statement here to include some states (nodes), Cyclone then will also find path(s) to these states. In this example, our goal is pretty simple just to find all possible strings with a length of 5. We compile this specification, and Cyclone automatically returns the following paths.

S->r1->r2->r2->r2->r1
S->r1->r1->r2->r2->r1
S->r1->r1->r1->r2->r1
S->r1->r2->r1->r2->r1
S->r1->r1->r2->r1->r1
S->q1->q1->q1->q1->q1
S->q1->q1->q2->q1->q1
S->q1->q2->q1->q1->q1
S->q1->q2->q2->q1->q1
S->q1->q2->q1->q2->q1
S->q1->q2->q2->q2->q1
S->q1->q1->q1->q2->q1
S->q1->q1->q2->q2->q1
S->r1->r1->r1->r1->r1
S->r1->r2->r1->r1->r1
S->r1->r2->r2->r1->r1

For example, the first path is translated to a string "baaab". Here is an exercise, can you use Cyclone to find all possible strings with a length of 5 but only those begin with an a ?

Tips:

They are multiple ways of doing it. One of the ways is to use the ! introduced from previous Section.

< Previous Next >