Commit 73800a26 authored by JACHIET Louis's avatar JACHIET Louis
Browse files

Update repo

parent 64bd91e1
......@@ -7,20 +7,20 @@ done;
for i in e9 e10 e11 e12 ; do
echo "" ; echo "------------------------------------------------" ;
echo "Translation to automaton $i…"
time ../trad/solver $i.mu compress > $i.auto
time -p ../trad/solver $i.mu compress > $i.auto
echo "" ; echo "------------------------------------------------" ;
echo "Translation to automaton n$i…"
time ../trad/solver n$i.mu compress > n$i.auto
time -p ../trad/solver n$i.mu compress > n$i.auto
done ;
echo "" ; echo "------------------------------------------------" ;
echo "Intersecting everything!";
echo "e9 ⊑ e10 U e11 U e12 => non sat of e9 ∩ ¬ e10 ∩ ¬ e11 ∩ ¬ e12 "
time (((((cat e9.auto ne10.auto | ../interAuto/inter) ;(cat ne11.auto ne12.auto | ../interAuto/inter)) | ../interAuto/inter ) ) | sed 's/.context//' ) | ../example/get_example_label.sh
time -p (((((cat e9.auto ne10.auto | ../interAuto/inter) ;(cat ne11.auto ne12.auto | ../interAuto/inter)) | ../interAuto/inter ) ) | sed 's/.context//' ) | ../example/get_example_label.sh
echo "" ; echo "" ;
echo "e9 ⊑ e10 U e11 U e12 modulo XHTML => non sat of e9 ∩ ¬ e10 ∩ ¬ e11 ∩ ¬ e12 ∩ XHTML "
time ((((((cat e9.auto ne10.auto | ../interAuto/inter) ;(cat ne11.auto ne12.auto | ../interAuto/inter)) | ../interAuto/inter ) ) | sed 's/.context//' ) ;cat ../xhtml_strict.auto) | ../intersect/inter
time -p ((((((cat e9.auto ne10.auto | ../interAuto/inter) ;(cat ne11.auto ne12.auto | ../interAuto/inter)) | ../interAuto/inter ) ) | sed 's/.context//' ) ;cat ../xhtml_strict.auto) | ../intersect/inter
echo "" ; echo "------------------------------------------------" ;
......
tr010.form 200557768
tr020.form 338984746
tr030.form 856928166
tr040.form 2436639805
tr010.form 214690002
tr020.form 378220410
tr030.form 830379590
tr040.form 2269975690
tr050.form 4827771658
tr060.form 9682643871
tr070.form 19080439042
tr080.form 32216831765
tr090.form 54430807760
tr0.form 85852728
tr110.form 114352687627
tr120.form 143528137249
tr130.form 206470573322
tr140.form 268835801901
tr150.form 331299885091
tr160.form 432590034353
......@@ -7,5 +7,10 @@ time (../trad/solver e2.mu compress ; ../trad/solver ne1.mu compress )| ../inter
(cat ne1.mu ; echo '&' ; cat e2.mu) > ne1e2
echo ""
echo "--------------------------------------------------"
echo -n "The full intersection ..."
time (../trad/solver e2.mu compress ; ../trad/solver ne1.mu compress )| ../interAuto/inter > /dev/null
echo ""
echo "--------------------------------------------------"
echo -n "The other method ..."
/usr/lib/jvm/java-8-openjdk/bin/java -jar solver.jar ne1e2 | sed -n 's/Computing Fixpoint\.*\[\(.*\)\]/\1/p'
......@@ -12,10 +12,8 @@ let uniq_id () =
let (get_label : (string list -> int)),list_labels = uniq_id ()
let get_type,list_types = uniq_id ()
(* let get_type,list_types = uniq_id () *)
let get_ith l i =
List.nth (List.rev l) i
let get_ith l i = List.nth (List.rev l) i
let trans = [|[];[];[]|]
......@@ -32,6 +30,13 @@ let add_transition label (s1:Sol.i) (s2:Sol.i) (s3:Sol.i) (c:int) =
;;
(*
Printing the output automaton, we remove non-coaccessible states, the
argument "trad" contains the translation from internal representation
of labels to their input (trad = identity when compression isn't used
*)
let show_automaton trad =
set_final Sol.notsol ;
let nb_types = (List.length (list_types ())) in
......@@ -55,7 +60,6 @@ let show_automaton trad =
for i = 0 to nb_types -1 do
if seen.(i) then incr access ;
done;
(* print_string "Number of accessibles states " ; print_int (!access) ; print_string " / " ; print_int nb_types ; print_newline () ; *)
let labels = Array.of_list ((List.rev(List.map trad (list_labels())))) in
let use_label = Array.mapi (fun i s -> (i==0) || (labels.(i-1)<>s)) labels in
let nb_labels = Array.fold_left (fun a e-> a+(if e then 1 else 0)) 0 use_label in
......@@ -66,7 +70,7 @@ let show_automaton trad =
and t2 = (ftrans trans.(2)) in
print_string "\n";
print_int nb_types ;
print_string " 0 1 " ; (* start state*)
print_string " 0 1 " ; (* start states *)
print_int (!final) ;
print_string " " ;
print_int (List.length t1 + List.length t2) ;
......@@ -86,7 +90,12 @@ let show_automaton trad =
(*
Printing a deterministic automaton
BETA_MODE not much tested !!!
*)
let get_automaton trad =
let rec uniq = function
......
......@@ -53,7 +53,7 @@ let lean f =
| Mu(l,f) ->
foo acc (replace l (List.assoc f l))
| True -> acc
| Var _ -> failwith "erreur, variable non remplacee"
| Var _ -> failwith "Error, unfolded var"
in
let rec num = function
......@@ -70,7 +70,7 @@ let lean f =
| Or(a,b) -> Bf.Or(mu_to_bf a, mu_to_bf b)
| Neg(a) -> Bf.neg (mu_to_bf a)
| Mu(l,f) -> mu_to_bf (replace l (List.assoc f l))
| Var _ -> failwith "erreur var non remplacee"
| Var _ -> failwith "Error, unfolded var"
| True -> Bf.Top
| f -> Bf.Litt (List.assoc f nl,false)
in
......
......@@ -43,6 +43,7 @@ let solve debug stats form plean =
Bf.simplify (List.fold_left (fun ac el -> Bf.Or(ac,el)) Bf.Bot (prog m))
in
(* neg_prog_form L prevents all formulas <i>φ to be true for i∈L *)
let neg_prog_form m =
Bf.neg (prog_form m)
in
......@@ -64,7 +65,7 @@ let solve debug stats form plean =
in
let interface =
let interface moda = (* moda = 1 ou moda = 2 *)
let interface moda = (* moda = 1 or moda = 2 *)
let foo l (form,id) = match form with
| Bf.Af_Prog(i,f) ->
if i = moda
......@@ -106,11 +107,13 @@ let solve debug stats form plean =
let compute c (s1,s2) flist sol =
let marque last_var_set set_sol =
let mark last_var_set set_sol =
let a = combine flist in
(* For each atom i we have set atom.(i) to bool Option mark_all
adds all the transition corresponding to the labels defined by
those atoms *)
let rec mark_all limit cur = function
| [] -> Auto.add_transition cur s1 s2 a c
| (s,i)::q ->
......@@ -121,7 +124,10 @@ let solve debug stats form plean =
| Some(true) -> mark_all limit (s::cur) q
| Some(false) -> mark_all limit cur q
in
(* We have found a transition from a set of transitions S but
maybe not all atoms are set, gen_all generate all variations of
atoms compatible with the the set S *)
let rec gen_all i s =
match Sol.get_type s with
| Sol.Bot -> ()
......@@ -134,10 +140,12 @@ let solve debug stats form plean =
gen_all (i+1) f ;
atom_val.(i) <- None) [false;true]
in
gen_all last_var_set set_sol ;
if not (Sol.mem fixed seen.(c))
then
begin
(* discovered a new accessible state *)
seen.(c) <- Sol.add fixed seen.(c) ;
todo.(c) <- a::todo.(c)
end
......@@ -162,7 +170,7 @@ let solve debug stats form plean =
if sol <> Sol.none
then
if to_fix = []
then marque i sol
then mark i sol
else
begin
let a,b = match Sol.get_type sol with
......@@ -223,7 +231,7 @@ let solve debug stats form plean =
print_newline () ;
let foo (x,y) =
Bf.print x;
print_string " <=sur le fils / sur parent ";
print_string " <= on child / on parent ";
print_int i ;
print_string "=> " ;
Bf.print y ;
......@@ -237,7 +245,7 @@ let solve debug stats form plean =
compute i (s1,s2) solved_interface.(i) (Sol.inter (Sol.inter s1 s2) no_parent.(3-i))
in
let marque_final (s1,s2) =
let mark_final (s1,s2) =
let sols = Sol.inter (Sol.inter s1 s2) sol_form in
let rec foo i c s =
if s <> Sol.none
......@@ -262,7 +270,7 @@ let solve debug stats form plean =
let f x = if i = 1 then (a,x) else (x,a) in
List.iter (fun x -> compute_side 1 (f x)) made.(3-i) ;
List.iter (fun x -> compute_side 2 (f x)) made.(3-i) ;
List.iter (fun x -> marque_final (f x)) made.(3-i) ;
List.iter (fun x -> mark_final (f x)) made.(3-i) ;
made.(i) <- a::made.(i) ;
true
in
......@@ -275,5 +283,5 @@ let solve debug stats form plean =
made.(1) <- [no_child_form.(1)] ;
todo.(2) <- [no_child_form.(2)] ;
fix_point () ;
if stats then show_stats ()
if stats && false then show_stats ()
......@@ -4,7 +4,7 @@
exception Lexing_error of string
let kwd_tbl = ["let", LET; "in", IN; "mu", MU;"T", TRUE ]
let kwd_tbl = ["let", LET; "in", IN; "mu", MU;"T", TRUE ; ".",POINT ]
let id_or_kwd s = try List.assoc s kwd_tbl with _ -> IDENT s
let line = ref 0
let newline () = incr line
......@@ -26,7 +26,6 @@ rule next_token = parse
| '&' { AND }
| ',' { COMMA }
| '~' { NOT }
| '.' { POINT }
| '(' { LEFTPAR }
| ')' { RIGHTPAR }
| '<' { LEFTPROG }
......
......@@ -21,7 +21,7 @@ let _ =
if Sys.argv.(i) = "debug" then debug := true ;
done ;
try
if !stats then print_string ("Opening file "^Sys.argv.(1)^"!\n") ;
if !debug then print_string ("Opening file "^Sys.argv.(1)^"!\n") ;
let c = open_in Sys.argv.(1) in
let lb = Lexing.from_channel c in
let f = (Mu.testfreevar (Parser.formfile Lexer.next_token lb)) in
......@@ -32,6 +32,12 @@ let _ =
if !lean then Mu.print f ;
let tlean,plean,form = Mu.lean f in
Sol.resize (tlean*tlean*200+7) ;
if !stats then
begin
print_string "Lean Size ";
print_int (List.length plean) ;
print_newline();
end ;
if !lean then
begin
print_string "\nLean :\n";
......
......@@ -2,9 +2,8 @@
rm -rf res/ ;
mkdir res ;
(for i in mu/* ; do
echo -n "(${i##mu/},"
(time -p (../trad/solver $i compress > res/${i##mu/} ; cat res/${i##mu} xhtml_strict.auto | ../intersect/inter)) 2>&1 | grep user | sed 's/user//' | tr -d "\n" | tr -d " "
echo -n ") "
done ;) | tee data.res
echo ""
for i in mu/* ; do
echo "${i##mu/}"
tim=$((time -p (../trad/solver $i stats compress > res/${i##mu/})) 2>&1 | grep user | sed 's/user//' | tr -d "\n" | tr -d " ")
echo $tim >> res/${i##mu/}
done ;
(let
$X7=((interval &
(let
$X6=(<-1><1>
(let
$X5=((bidder &
(let
$X4=(<-1>(open_auction &
(let
$X3=(<-1>
(let
$X1=((~<-1>T & ~<-2>T & ~<2>T & T) | $X2),
$X2=(<-1>$X1 | <-2>$X2)
in
$X1) | <-2>$X3)
in
$X3)) | <-2>$X4)
in
$X4)) | <2>$X5)
in
$X5) | <-2>$X6)
in
$X6)) | <1>$X7 | <2>$X7)
in
$X7)
(let
$X9=((interval &
(let
$X8=(<-1><1>
(let
$X7=((bidder &
(let
$X6=(<-1><1>
(let
$X5=((bidder &
(let
$X4=(<-1>(open_auction &
(let
$X3=(<-1>
(let
$X1=((~<-1>T & ~<-2>T & ~<2>T & T) | $X2),
$X2=(<-1>$X1 | <-2>$X2)
in
$X1) | <-2>$X3)
in
$X3)) | <-2>$X4)
in
$X4)) | <2>$X5)
in
$X5) | <-2>$X6)
in
$X6)) | <2>$X7)
in
$X7) | <-2>$X8)
in
$X8)) | <1>$X9 | <2>$X9)
in
$X9)
(let
$X11=((interval &
(let
$X10=(<-1><1>
(let
$X9=((bidder &
(let
$X8=(<-1><1>
(let
$X7=((bidder &
(let
$X6=(<-1><1>
(let
$X5=((bidder &
(let
$X4=(<-1>(open_auction &
(let
$X3=(<-1>
(let
$X1=((~<-1>T & ~<-2>T & ~<2>T & T) | $X2),
$X2=(<-1>$X1 | <-2>$X2)
in
$X1) | <-2>$X3)
in
$X3)) | <-2>$X4)
in
$X4)) | <2>$X5)
in
$X5) | <-2>$X6)
in
$X6)) | <2>$X7)
in
$X7) | <-2>$X8)
in
$X8)) | <2>$X9)
in
$X9) | <-2>$X10)
in
$X10)) | <1>$X11 | <2>$X11)
in
$X11)
(let
$X6=((keyword &
(let
$X5=(<-1>((parlist & <1>
(let
$X4=((keyword &
(let
$X3=(<-1>
(let
$X1=((~<-1>T & ~<-2>T & ~<2>T & T) | $X2),
$X2=(<-1>$X1 | <-2>$X2)
in
$X1) | <-2>$X3)
in
$X3)) | <1>$X4 | <2>$X4)
in
$X4)) | $X5) | <-2>$X5)
in
$X5)) | <1>$X6 | <2>$X6)
in
$X6)
(let
$X8=((keyword &
(let
$X7=(<-1>((parlist & <1>
(let
$X6=((keyword &
(let
$X5=(<-1>((parlist & <1>
(let
$X4=((keyword &
(let
$X3=(<-1>
(let
$X1=((~<-1>T & ~<-2>T & ~<2>T & T) | $X2),
$X2=(<-1>$X1 | <-2>$X2)
in
$X1) | <-2>$X3)
in
$X3)) | <1>$X4 | <2>$X4)
in
$X4)) | $X5) | <-2>$X5)
in
$X5)) | <1>$X6 | <2>$X6)
in
$X6)) | $X7) | <-2>$X7)
in
$X7)) | <1>$X8 | <2>$X8)
in
$X8)
(let
$X10=((keyword &
(let
$X9=(<-1>((parlist & <1>
(let
$X8=((keyword &
(let
$X7=(<-1>((parlist & <1>
(let
$X6=((keyword &
(let
$X5=(<-1>((parlist & <1>
(let
$X4=((keyword &
(let
$X3=(<-1>
(let
$X1=((~<-1>T & ~<-2>T & ~<2>T & T) | $X2),
$X2=(<-1>$X1 | <-2>$X2)
in
$X1) | <-2>$X3)
in
$X3)) | <1>$X4 | <2>$X4)
in
$X4)) | $X5) | <-2>$X5)
in
$X5)) | <1>$X6 | <2>$X6)
in
$X6)) | $X7) | <-2>$X7)
in
$X7)) | <1>$X8 | <2>$X8)
in
$X8)) | $X9) | <-2>$X9)
in
$X9)) | <1>$X10 | <2>$X10)
in
$X10)
(let
$X6=((bidder &
(let
$X5=<2>((bidder &
(let
$X4=<-2>((bidder &
(let
$X3=(<-1>
(let
$X1=((~<-1>T & ~<-2>T & ~<2>T & T) | $X2),
$X2=(<-1>$X1 | <-2>$X2)
in
$X1) | <-2>$X3)
in
$X3)) | $X4)
in
$X4)) | $X5)
in
$X5)) | <1>$X6 | <2>$X6)
in
$X6)
(let
$X8=((bidder &
(let
$X7=<2>((bidder &
(let
$X6=<-2>((bidder &
(let
$X5=<2>((bidder &
(let
$X4=<-2>((bidder &
(let
$X3=(<-1>
(let
$X1=((~<-1>T & ~<-2>T & ~<2>T & T) | $X2),
$X2=(<-1>$X1 | <-2>$X2)
in
$X1) | <-2>$X3)
in
$X3)) | $X4)
in
$X4)) | $X5)
in
$X5)) | $X6)
in
$X6)) | $X7)
in
$X7)) | <1>$X8 | <2>$X8)
in
$X8)
(let
$X10=((bidder &
(let
$X9=<2>((bidder &
(let
$X8=<-2>((bidder &
(let
$X7=<2>((bidder &
(let
$X6=<-2>((bidder &
(let
$X5=<2>((bidder &
(let
$X4=<-2>((bidder &
(let
$X3=(<-1>
(let
$X1=((~<-1>T & ~<-2>T & ~<2>T & T) | $X2),
$X2=(<-1>$X1 | <-2>$X2)
in
$X1) | <-2>$X3)
in
$X3)) | $X4)
in
$X4)) | $X5)
in
$X5)) | $X6)
in
$X6)) | $X7)
in
$X7)) | $X8)
in
$X8)) | $X9)
in
$X9)) | <1>$X10 | <2>$X10)
in
$X10)
(let
$X14=((keyword &
(let
$X12=(
(let
$X11=<2>(
(let
$X9=((keyword &
(let
$X7=(
(let
$X6=<-2>(
(let
$X4=((keyword &
(let
$X3=(<-1>
(let
$X1=((~<-1>T & ~<-2>T & ~<2>T & T) | $X2),
$X2=(<-1>$X1 | <-2>$X2)
in
$X1) | <-2>$X3)
in
$X3)) | <1>$X5),
$X5=($X4 | <2>$X4)
in
$X4) | $X6)
in
$X6) | $X8),
$X8=(<-1>$X7 | <-2>$X8)
in
$X7)) | <1>$X10),
$X10=($X9 | <2>$X9)
in
$X9) | $X11)
in
$X11) | $X13),
$X13=(<-1>$X12 | <-2>$X13)
in
$X12)) | <1>$X14 | <2>$X14)
in
$X14)