open Automaton[States, Alphabet, NoInput]

-- A simple example for checking the Automaton module.
-- copyright Richard St-Denis, Universite de Sherbrooke, 2015.

enum States { s0, s1, s2, s3, s4, s5, s6, s7, s8, s9 }
enum Alphabet { a, b, c, d, e }

abstract sig NoInput { }
one sig eps extends NoInput { } -- Comment if the automaton is nondeterministic

one sig A extends Automaton { }
{
 states = s0 + s1 + s2 + s3 + s4 + s5 + s6 + s7 + s8 + s9
 labels = a + b + c + d + e
 transition = s0->a->s1 + s1->b->s2 + s2->c->s3 + s3->d->s0 + s3->e->s5
            + s0->a->s6 + s6->eps->s3   -- two forms of nondeterminism
            + s7->a->s6                 -- unreachable state (s7)
            + s5->c->s8 + s8->c->s9     -- uncoreachable states (s8 and s9)
 initialState = s0
 finalStates = s5 + s6
}

fact
{
 -- no NoInput   -- Remove the comment if the automaton is deterministic
 no SilentEvents
}

-- one sig B extends Automaton { }

one sig C extends Automaton { }
{
 states = s0 + s1 + s2 + s3 + s5 + s6
 labels = a + b + c + d + e
 transition = s0->a->s1 + s1->b->s2 + s2->c->s3 + s3->d->s0 + s3->e->s5
            + s0->a->s6 + s6->eps->s3
 initialState = s0
 finalStates = s5 + s6
}

one sig D extends Automaton { }
{ -- use to check the instances of a walk
 states = s0 + s1 + s2 + s3 + s4 + s5 + s6
 labels = a + b
 transition = s0->a->s1 + s0->a->s2
            + s1->b->s3 + s1->b->s4
            + s2->b->s5 + s2->b->s6
 initialState = s0
 finalStates = s3 + s4 + s5 + s6
}

-- one sig w extends Walk { }
-- { -- to check the instances of a walk
--  stg = D
-- }

one sig w extends Walk { }
{ -- to check Extension
 edges[0] = a
 edges[1] = b
 edges[2] = c
 edges[3] = d
 edges[4] = a
 edges[5] = eps
 edges[6] = e
 stg = C
}

one sig w1 extends Walk { }
{ -- to check Extension
 walkLength[w1] = 0
 stg = C
}

one sig t1 extends Trace { }
{
 t1 = walkToTrace[w, a+c+e]
}

one sig w2 extends Walk { }
{ -- to check Extension
 stg = C
}

one sig w3 extends Walk { }
-- to ckeck projectWalk


pred findAWalk[x: one Walk, y: one Walk, L: set Alphabet+NoInput]
{ --  find a walk with the same projection as another walk
 x.stg = y.stg
 (not x.edges = y.edges)
 projectWalk[y, L] = projectWalk[x, L]
}


run { } for 1 but 5 Int, 15 seq, 3 Walk

check isDeterministicNo { A.isDeterministic } for 1
      but 5 Int, 10 seq, 3 Walk
-- use nonDeterministicTransitions[A] and epsTransitions[A]
--   in the evaluator to see the counterexamples

check isTrimNo { A.isTrim } for 1
      but 5 Int, 10 seq, 3 Walk
-- use getReachableStates[A, A.initialState, A.labels+NoInput] and
--   getCoreachableStates[A, A.finalStates, A.labels+NoInput] in the
--   evaluator to see the counterexamples

--run Trim { trim[B, A, A.labels+NoInput] } for 1
--    but 5 Int, 4 seq, 1 Walk

check isARestrictionYes { C.isARestriction[A, s0+s1+s2+s3+s5+s6] } for 1
      but 5 Int, 10 seq, 3 Walk
check isARestrictionNo { C.isARestriction[A, s0+s1+s2+s5+s6] } for 1
      but 5 Int, 10 seq, 3 Walk

check restriction { let B = restriction[A, s0+s1+s2+s3+s5+s6] |
                            B.states = C.states
                        and B.initialState = C.initialState
                        and B.finalStates = C.finalStates
                        and B.labels = C.labels
                        and B.transition = C.transition } for 1
      but 5 Int, 10 seq, 3 Walk

check isSubautomatonYes { C.isSubautomaton[A] } for 1
      but 5 Int, 10 seq, 3 Walk
check isSubautomatonNo { A.isSubautomaton[C] } for 1
      but 5 Int, 10 seq, 3 Walk
run extension { w2 = extension[w1,a] } for 1
    but 5 Int, 10 seq, 3 Walk
check isAnExtensionYes {isAnExtension [w1, a] } for 1
      but 5 Int, 10 seq, 3 Walk
run findAWalk { w3.findAWalk[w, a+b+c+d] } for 1
    but 5 Int, 10 seq, 3 Walk