Guest User

Untitled

a guest
Nov 17th, 2018
104
0
Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
text 1.85 KB | None | 0 0
  1. Require Import List.
  2. Require Import ListSet.
  3. Require Import Ascii.
  4. Require Import String.
  5.  
  6. Definition state := nat.
  7. Definition stateset := set state.
  8. Definition symbol := ascii.
  9. Definition symbolset := set symbol.
  10.  
  11. Inductive transition : Type :=
  12. | TepsilonCall: state -> (state*state) -> transition
  13. | Transition: (state*symbol) -> state -> transition.
  14.  
  15. Definition transitionset := set transition.
  16.  
  17. Inductive nrfa : Type :=
  18. | NRFA:
  19. forall (initial: state) (alphabet: symbolset) (states: stateset)
  20. (finals: stateset) (calls: stateset) (transitions: transitionset), nrfa.
  21.  
  22. Axiom s_in : forall (s:state) ss, {set_In s ss} + {~set_In s ss}.
  23.  
  24. Fixpoint get_calls_t (trans:transitionset) (r:transitionset) : transitionset :=
  25. match trans with
  26. | nil => r
  27. | t::ts =>
  28. match t with
  29. | TepsilonCall _ _ => get_calls_t ts (t::r)
  30. | _ => get_calls_t ts (t::r)
  31. end
  32. end.
  33.  
  34. Fixpoint get_calls (m:nrfa) : transitionset :=
  35. match m with
  36. | NRFA initial alphabet states finals calls transitions =>
  37. get_calls_t transitions nil
  38. end.
  39.  
  40.  
  41. Fixpoint isCircular (s:state) (cs:stateset) (transitions:transitionset) : Prop :=
  42. if (s_in s cs) then True
  43. else
  44. let fix isCircular_ts (trans:transitionset) :=
  45. match trans with
  46. | nil => False
  47. | t::ts =>
  48. match t with
  49. | TepsilonCall s' (call, _) => (eq s' s) /\ (isCircular call (s::call::cs) transitions)
  50. | _ => False
  51. end
  52. \/ (isCircular_ts ts)
  53. end
  54. in isCircular_ts transitions.
  55.  
  56. Definition isCircularM (m:nrfa) :=
  57. match m with
  58. | NRFA initial alphabet states finals calls transitions =>
  59. isCircular initial nil
  60. end.
Add Comment
Please, Sign In to add comment