Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- Require Import List.
- Require Import ListSet.
- Require Import Ascii.
- Require Import String.
- Definition state := nat.
- Definition stateset := set state.
- Definition symbol := ascii.
- Definition symbolset := set symbol.
- Inductive transition : Type :=
- | TepsilonCall: state -> (state*state) -> transition
- | Transition: (state*symbol) -> state -> transition.
- Definition transitionset := set transition.
- Inductive nrfa : Type :=
- | NRFA:
- forall (initial: state) (alphabet: symbolset) (states: stateset)
- (finals: stateset) (calls: stateset) (transitions: transitionset), nrfa.
- Axiom s_in : forall (s:state) ss, {set_In s ss} + {~set_In s ss}.
- Fixpoint get_calls_t (trans:transitionset) (r:transitionset) : transitionset :=
- match trans with
- | nil => r
- | t::ts =>
- match t with
- | TepsilonCall _ _ => get_calls_t ts (t::r)
- | _ => get_calls_t ts (t::r)
- end
- end.
- Fixpoint get_calls (m:nrfa) : transitionset :=
- match m with
- | NRFA initial alphabet states finals calls transitions =>
- get_calls_t transitions nil
- end.
- Fixpoint isCircular (s:state) (cs:stateset) (transitions:transitionset) : Prop :=
- if (s_in s cs) then True
- else
- let fix isCircular_ts (trans:transitionset) :=
- match trans with
- | nil => False
- | t::ts =>
- match t with
- | TepsilonCall s' (call, _) => (eq s' s) /\ (isCircular call (s::call::cs) transitions)
- | _ => False
- end
- \/ (isCircular_ts ts)
- end
- in isCircular_ts transitions.
- Definition isCircularM (m:nrfa) :=
- match m with
- | NRFA initial alphabet states finals calls transitions =>
- isCircular initial nil
- end.
Add Comment
Please, Sign In to add comment