Cyclone: A Graph-Based Specification Language

/**
 * A simple counting machine has three instructions only:
 * increment the counter.
 * decrement the counter.
 * reset the counter.
 */
graph CountingMachine { 
    int c;

    start normal node R { c = 0;     }
    normal       node I { c = c + 1; }
    normal       node D { c = c - 1; }

    edge { R -> I, D    }
    edge { I -> I, D, R }
    edge { D -> I, D, R }

    goal{
        /**
         * Find all possible of instruction sequences that use 6 instructions 
         * to make the counter=3 and must use the decrement instruction somewhere.
         */

        assert c == 3;
        enumerate for 5 condition (D) reach (R,I,D)
    }
}