all:
	@echo "type make:"
	@echo "split -> 12 canonical proofs with gbac symbolic algo"
	@echo "lesar -> same with the standard lustre MC"
	@echo "full -> full single proof with gbac symbolic algo"
	@echo "test -> simulation with luciole" 
	@echo "        a full installation of lustre"
	@echo "        is required for that ..."


test: model.lus
	luciole model.lus test

full: proof.ba
	gbac -f -v proof.ba

split: model.lus
	@\
nlist=`cat model.lus | grep verif_ | wc -l`;\
echo "Necessary proofs: $$nlist";\
vlist=`cat model.lus | grep verif_`;\
for x in $$vlist ; do \
echo "----- $$x ------";\
lus2ec model.lus $$x; \
ec2ba $$x.ec; \
gbac -f $$x.ba -v; \
done

lesar: model.lus
	@\
nlist=`cat model.lus | grep verif_ | wc -l`;\
echo "Necessary proofs: $$nlist";\
vlist=`cat model.lus | grep verif_`;\
for x in $$vlist ; do \
echo "----- $$x ------";\
lesar model.lus $$x -v -merge -states 10000000;\
done

proof.ba: proof.ec
	ec2ba proof.ec

proof.ec: model.lus
	lus2ec model.lus proof

SRC=\
  UsrIntBinary4.lus \
  UsrIntBinary.lus \
  BoolArrays.lus \
  make_model.ml

model.lus: $(SRC)
	ocaml make_model.ml > model.lus

clean:
	rm -f *.ec *.ba model.lus