From eddc01e1c9e644bf62112c8a8121aa40d59715b4 Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Tue, 27 Nov 2018 09:40:44 +0000 Subject: [PATCH] Cleanup. --- examples/academic_paper/Monitor_Example.thy | 46 --------------------- 1 file changed, 46 deletions(-) delete mode 100644 examples/academic_paper/Monitor_Example.thy diff --git a/examples/academic_paper/Monitor_Example.thy b/examples/academic_paper/Monitor_Example.thy deleted file mode 100644 index 1b3ca91b..00000000 --- a/examples/academic_paper/Monitor_Example.thy +++ /dev/null @@ -1,46 +0,0 @@ -theory Monitor_Example - imports "../../ontologies/scholarly_paper" -begin - - -ML\ -val term = @{term "(title ~~ - \subtitle\ ~~ - \author\\<^sup>+ ~~ - abstract ~~ - introduction ~~ - \technical || example\\<^sup>+ ~~ - conclusion ~~ - bibliography)"} -\ - -ML\ -val alpha = (RegExpInterface.alphabet [term]); -val DA as (init,(next,fin)) = RegExpInterface.rexp_term2da alpha term ; -RegExpChecker.accepts DA [0,2,3,4,5,6,7,8]; -\ - -ML\ -(* simulation with low-level interface RegExpChecker generated from AFP Functional Automata module*) -val S0 = init -val E1 = RegExpChecker.enabled DA S0 [0,1,2,3,4,5,6,7,8]; -val S1 = next 0 init; -val E2 = RegExpChecker.enabled DA S1 [0,1,2,3,4,5,6,7,8]; -val S2 = next 2 S1; (* uffz. it works. *) -val E3 = RegExpChecker.enabled DA S2 [0,1,2,3,4,5,6,7,8]; -val S3 = next 3 S2; (* uffz. it works. *) -\ - -ML\ -(* simulation with high-level interface RegExpInterface *) - -RegExpInterface.enabled DA alpha; -val DA' = RegExpInterface.next DA alpha "scholarly_paper.title"; -RegExpInterface.enabled DA' alpha; -val DA'' = RegExpInterface.next DA' alpha "scholarly_paper.author"; -RegExpInterface.enabled DA'' alpha; -\ - - - -end