From 70d587d2e3eb5640e812f8a9e7398371d031f47f Mon Sep 17 00:00:00 2001 From: Peter Fontana Date: Mon, 20 Jan 2020 20:53:04 -0500 Subject: [PATCH 01/11] Added vacuity command-line options (implementation in progress) --- .DS_Store | Bin 0 -> 8196 bytes pes.timed/prover_options.hh | 8 ++++++++ pes.timed/timesolver-ta.cc | 16 +++++++++++++--- 3 files changed, 21 insertions(+), 3 deletions(-) create mode 100644 .DS_Store diff --git a/.DS_Store b/.DS_Store new file mode 100644 index 0000000000000000000000000000000000000000..5139a34d032d7cc2e8087317d0962ea13566ab17 GIT binary patch literal 8196 zcmeHM&2G~`5S~q1nyBiJDiG!7OK&AgXd6@{q%=*1A_1*%RD=MvabmR=jvXZqX$YzE z4&30*gK*>pcn4krzWr(BIIfUdgaYhFGqYaLx4Zs!JT> zKhI^NBvi{SSOz>%z3lom%k`}ZU)`V?&Gy|Fe&A@apfM+%@sY{;w@~qaH0nNaF z$pDWJ287#!vO{S_=ztO_0PGB!ML`{TfWR2a7L*-IE1>98W)Dn3nMyI3gyX!y-C+yL z4yBcFViHbFjm%Vr!o=vn8N!`dL0YXf1Db(J26*m1OBQv=A$Kf)=Qq*=$l4E41T^Gn zb=ysq>3_AFuG0>(*>5b7oSD5bmrCQeka}&N`du@q2Ay`X+Iq>44ywVarRo*mcSrTA zb?DgLqve~sz86#-&u$5@Q@7#r>bc|9{ch3kc=fjE$CM}dIO(J1JNy|Hd==C=ofbn5n6?qT`3(R>RNB zbU-htOi$@i#QQwrouoSXREv0hkN5g#*HN($S;G|8>RZ2I-%ng=gt>X_+A{Xx9(JG!9lLWAUn2aa#a$xzxdYbiXpBi_evOzi&bRW2 zHJjPZ>&KcHb|S1V;;!EV-}{I>0iuqN6)@=#>^G@5zIR2m{t$}RE0_Q4W$(jD3OlC uigX-y^uZ8y1FjrXP Date: Fri, 31 Jan 2020 22:32:44 -0500 Subject: [PATCH 02/11] First iteration of simple vacuity checking (in progress) added --- .DS_Store | Bin 8196 -> 10244 bytes examples/ExampleGenerators/Makefile | 521 +++++++++++-- pes.timed/ExprNode.cc | 368 +++++++++ pes.timed/ExprNode.hh | 270 ++++++- pes.timed/proof.hh | 201 +++-- pes.timed/prover_options.hh | 8 +- pes.timed/test/dbmlisttest.cc | 441 ----------- pes.timed/test/dbmtest.cc | 1078 --------------------------- pes.timed/test/parsetest.cc | 58 -- pes.timed/test/prooftest.cc | 319 -------- pes.timed/timesolver-ta.cc | 62 +- pes.timed/transition.hh | 2 +- 12 files changed, 1276 insertions(+), 2052 deletions(-) delete mode 100644 pes.timed/test/dbmlisttest.cc delete mode 100644 pes.timed/test/dbmtest.cc delete mode 100644 pes.timed/test/parsetest.cc delete mode 100644 pes.timed/test/prooftest.cc diff --git a/.DS_Store b/.DS_Store index 5139a34d032d7cc2e8087317d0962ea13566ab17..f134e5ba599dde098fb024579c7068ca5111cba3 100644 GIT binary patch literal 10244 zcmeHMPfr_16n|rrVut|Bzowv8vOtll29O;hq*RJx3?xNL0>u`^C8@Kv7qiNG*VwkVPck&Yzx?kTtWQ4Dw{vs)kj?o6^G@SHuX!2*e1)2*e1)2wV*W zuxIm>8uDnI#|Xp-#0XpnV6FX@6`d^WR*fnsq!DmoC$Vnfg{Z=$*^~h<-ZvwwoTZZnq+3asDksP@8 z&R{By-*D=A@xVGNx~kiD3aY)w-?miupeoBH%Q7y?YIR4~jw;IJs%5&WZfdp=*6SKr zo_(g9b?c~LwavOC^c1}YZYNz)rcY0omvZx&J4?B<`OIl9dv9qzb9edP*;zVu^H%Qu z#*1d>8|*=HF(j+_ zWY@@oM2Ggpyz_DNtP?)_jQM7NCPKae>n5!s-$!rS7>kQ>^&JlZm4MFcKAjI`U!34L z*my|BkHKTea2&bK2n@JvU={{pZyM(cE3tf7NSf80^&=MG9 zlIlRa7P9qc$d=@KYyC=&FXU4xpnHs!(}Xt}9O)oRB3AjmsE7ZG;dLjQozLW!|A#o# zGtv-p3N^5*EaV(FSFX~9ezBZky#-d~L?3y+R*&G*2B;d|5%_!rw2bu8;*cF)@jR9V zWRtL=Q#Cl_JZc5FhUhVTb(PlPuSMjMelFrp(Rohn0hF0i2H`JzY*?{=JF4_ zg^#>~LUUe$Hy{$Yb` zn$5D?>@K^{9^q5xwKFG$4W3IK>FW2*e0n2?UZ}FEaf5|9b!b|F1+}<4(i~#0b0| z1lYh@ajgK|-NRqlOac`dJTLI@#QDxWDnyWR7G5tt$K!>6j{i{BWjW;u?RiPhJu1Xe hFT_E;ulcY2&ww}m9WuWE^KWGf_+l2{|KHGB{0}K(+hPC! delta 197 zcmZn(XmOBWU|?W$DortDU;r^WfEYvza8E20o2aKKEDDkb@);OXJah7slXCKtHWp4} zpV+{^nVo}$gHd#|kw7Nni09p%j4#VVl Po~e`hMVzo1kii51eoHGm diff --git a/examples/ExampleGenerators/Makefile b/examples/ExampleGenerators/Makefile index b216ca3..abc85a0 100644 --- a/examples/ExampleGenerators/Makefile +++ b/examples/ExampleGenerators/Makefile @@ -1,55 +1,472 @@ -CC = g++ -CCOPTS = -c -g - -all: csma fddi fischer grc leader pathos - -csma: csma.o - $(CC) -o csma csma.o - -csma.o: csma.cc CsmaModel.hh - $(CC) $(CCOPTS) csma.cc - -fddi: fddi.o - $(CC) -o fddi fddi.o - -fddi.o: fddi.cc FddiModel.hh - $(CC) $(CCOPTS) fddi.cc - -fischer: fischer.o - $(CC) -o fischer fischer.o - -fischer.o: fischer.cc FischerModel.hh - $(CC) $(CCOPTS) fischer.cc - -grc: grc.o - $(CC) -o grc grc.o - -grc.o: grc.cc GrcModel.hh - $(CC) $(CCOPTS) grc.cc - -leader: leader.o - $(CC) -o leader leader.o - -leader.o: leader.cc LeaderModel.hh - $(CC) $(CCOPTS) leader.cc - -pathos: pathos.o - $(CC) -o pathos pathos.o - -pathos.o: pathos.cc PathosModel.hh - $(CC) $(CCOPTS) pathos.cc +# CMAKE generated file: DO NOT EDIT! +# Generated by "Unix Makefiles" Generator, CMake Version 3.16 +# Default target executed when no arguments are given to make. +default_target: all + +.PHONY : default_target + +# Allow only one "make -f Makefile2" at a time, but pass parallelism. +.NOTPARALLEL: + + +#============================================================================= +# Special targets provided by cmake. + +# Disable implicit rules so canonical targets will work. +.SUFFIXES: + + +# Remove some rules from gmake that .SUFFIXES does not remove. +SUFFIXES = + +.SUFFIXES: .hpux_make_needs_suffix_list + + +# Suppress display of executed commands. +$(VERBOSE).SILENT: + + +# A target that is always out of date. +cmake_force: + +.PHONY : cmake_force + +#============================================================================= +# Set environment variables for the build. + +# The shell in which to execute make rules. +SHELL = /bin/sh + +# The CMake executable. +CMAKE_COMMAND = /usr/local/Cellar/cmake/3.16.2/bin/cmake + +# The command to remove a file. +RM = /usr/local/Cellar/cmake/3.16.2/bin/cmake -E remove -f + +# Escaping for special characters. +EQUALS = = + +# The top-level source directory on which CMake was run. +CMAKE_SOURCE_DIR = /Users/pfontana/Documents/GradSchoolClasses/CSDSvn/pfontana/Research/Cleaveland/Code/github_pestimed/TimeSolver + +# The top-level build directory on which CMake was run. +CMAKE_BINARY_DIR = /Users/pfontana/Documents/GradSchoolClasses/CSDSvn/pfontana/Research/Cleaveland/Code/github_pestimed/TimeSolver + +#============================================================================= +# Targets provided globally by CMake. + +# Special rule for the target install/strip +install/strip: preinstall + @$(CMAKE_COMMAND) -E cmake_echo_color --switch=$(COLOR) --cyan "Installing the project stripped..." + /usr/local/Cellar/cmake/3.16.2/bin/cmake -DCMAKE_INSTALL_DO_STRIP=1 -P cmake_install.cmake +.PHONY : install/strip + +# Special rule for the target install/strip +install/strip/fast: preinstall/fast + @$(CMAKE_COMMAND) -E cmake_echo_color --switch=$(COLOR) --cyan "Installing the project stripped..." + /usr/local/Cellar/cmake/3.16.2/bin/cmake -DCMAKE_INSTALL_DO_STRIP=1 -P cmake_install.cmake +.PHONY : install/strip/fast + +# Special rule for the target install/local +install/local: preinstall + @$(CMAKE_COMMAND) -E cmake_echo_color --switch=$(COLOR) --cyan "Installing only the local directory..." + /usr/local/Cellar/cmake/3.16.2/bin/cmake -DCMAKE_INSTALL_LOCAL_ONLY=1 -P cmake_install.cmake +.PHONY : install/local + +# Special rule for the target install/local +install/local/fast: preinstall/fast + @$(CMAKE_COMMAND) -E cmake_echo_color --switch=$(COLOR) --cyan "Installing only the local directory..." + /usr/local/Cellar/cmake/3.16.2/bin/cmake -DCMAKE_INSTALL_LOCAL_ONLY=1 -P cmake_install.cmake +.PHONY : install/local/fast + +# Special rule for the target rebuild_cache +rebuild_cache: + @$(CMAKE_COMMAND) -E cmake_echo_color --switch=$(COLOR) --cyan "Running CMake to regenerate build system..." + /usr/local/Cellar/cmake/3.16.2/bin/cmake -S$(CMAKE_SOURCE_DIR) -B$(CMAKE_BINARY_DIR) +.PHONY : rebuild_cache + +# Special rule for the target rebuild_cache +rebuild_cache/fast: rebuild_cache + +.PHONY : rebuild_cache/fast + +# Special rule for the target edit_cache +edit_cache: + @$(CMAKE_COMMAND) -E cmake_echo_color --switch=$(COLOR) --cyan "Running CMake cache editor..." + /usr/local/Cellar/cmake/3.16.2/bin/ccmake -S$(CMAKE_SOURCE_DIR) -B$(CMAKE_BINARY_DIR) +.PHONY : edit_cache + +# Special rule for the target edit_cache +edit_cache/fast: edit_cache + +.PHONY : edit_cache/fast + +# Special rule for the target test +test: + @$(CMAKE_COMMAND) -E cmake_echo_color --switch=$(COLOR) --cyan "Running tests..." + /usr/local/Cellar/cmake/3.16.2/bin/ctest --force-new-ctest-process $(ARGS) +.PHONY : test + +# Special rule for the target test +test/fast: test + +.PHONY : test/fast + +# Special rule for the target list_install_components +list_install_components: + @$(CMAKE_COMMAND) -E cmake_echo_color --switch=$(COLOR) --cyan "Available install components are: \"Unspecified\"" +.PHONY : list_install_components + +# Special rule for the target list_install_components +list_install_components/fast: list_install_components + +.PHONY : list_install_components/fast + +# Special rule for the target install +install: preinstall + @$(CMAKE_COMMAND) -E cmake_echo_color --switch=$(COLOR) --cyan "Install the project..." + /usr/local/Cellar/cmake/3.16.2/bin/cmake -P cmake_install.cmake +.PHONY : install + +# Special rule for the target install +install/fast: preinstall/fast + @$(CMAKE_COMMAND) -E cmake_echo_color --switch=$(COLOR) --cyan "Install the project..." + /usr/local/Cellar/cmake/3.16.2/bin/cmake -P cmake_install.cmake +.PHONY : install/fast + +# The main all target +all: cmake_check_build_system + cd /Users/pfontana/Documents/GradSchoolClasses/CSDSvn/pfontana/Research/Cleaveland/Code/github_pestimed/TimeSolver && $(CMAKE_COMMAND) -E cmake_progress_start /Users/pfontana/Documents/GradSchoolClasses/CSDSvn/pfontana/Research/Cleaveland/Code/github_pestimed/TimeSolver/CMakeFiles /Users/pfontana/Documents/GradSchoolClasses/CSDSvn/pfontana/Research/Cleaveland/Code/github_pestimed/TimeSolver/examples/ExampleGenerators/CMakeFiles/progress.marks + cd /Users/pfontana/Documents/GradSchoolClasses/CSDSvn/pfontana/Research/Cleaveland/Code/github_pestimed/TimeSolver && $(MAKE) -f CMakeFiles/Makefile2 examples/ExampleGenerators/all + $(CMAKE_COMMAND) -E cmake_progress_start /Users/pfontana/Documents/GradSchoolClasses/CSDSvn/pfontana/Research/Cleaveland/Code/github_pestimed/TimeSolver/CMakeFiles 0 +.PHONY : all + +# The main clean target clean: - rm -f csma - rm -f csma.o - rm -f fddi - rm -f fddi.o - rm -f fischer - rm -f fischer.o - rm -f grc - rm -f grc.o - rm -f leader - rm -f leader.o - rm -f pathos - rm -f pathos.o + cd /Users/pfontana/Documents/GradSchoolClasses/CSDSvn/pfontana/Research/Cleaveland/Code/github_pestimed/TimeSolver && $(MAKE) -f CMakeFiles/Makefile2 examples/ExampleGenerators/clean +.PHONY : clean + +# The main clean target +clean/fast: clean + +.PHONY : clean/fast + +# Prepare targets for installation. +preinstall: all + cd /Users/pfontana/Documents/GradSchoolClasses/CSDSvn/pfontana/Research/Cleaveland/Code/github_pestimed/TimeSolver && $(MAKE) -f CMakeFiles/Makefile2 examples/ExampleGenerators/preinstall +.PHONY : preinstall + +# Prepare targets for installation. +preinstall/fast: + cd /Users/pfontana/Documents/GradSchoolClasses/CSDSvn/pfontana/Research/Cleaveland/Code/github_pestimed/TimeSolver && $(MAKE) -f CMakeFiles/Makefile2 examples/ExampleGenerators/preinstall +.PHONY : preinstall/fast + +# clear depends +depend: + cd /Users/pfontana/Documents/GradSchoolClasses/CSDSvn/pfontana/Research/Cleaveland/Code/github_pestimed/TimeSolver && $(CMAKE_COMMAND) -S$(CMAKE_SOURCE_DIR) -B$(CMAKE_BINARY_DIR) --check-build-system CMakeFiles/Makefile.cmake 1 +.PHONY : depend + +# Convenience name for target. +examples/ExampleGenerators/CMakeFiles/grc.dir/rule: + cd /Users/pfontana/Documents/GradSchoolClasses/CSDSvn/pfontana/Research/Cleaveland/Code/github_pestimed/TimeSolver && $(MAKE) -f CMakeFiles/Makefile2 examples/ExampleGenerators/CMakeFiles/grc.dir/rule +.PHONY : examples/ExampleGenerators/CMakeFiles/grc.dir/rule + +# Convenience name for target. +grc: examples/ExampleGenerators/CMakeFiles/grc.dir/rule + +.PHONY : grc + +# fast build rule for target. +grc/fast: + cd /Users/pfontana/Documents/GradSchoolClasses/CSDSvn/pfontana/Research/Cleaveland/Code/github_pestimed/TimeSolver && $(MAKE) -f examples/ExampleGenerators/CMakeFiles/grc.dir/build.make examples/ExampleGenerators/CMakeFiles/grc.dir/build +.PHONY : grc/fast + +# Convenience name for target. +examples/ExampleGenerators/CMakeFiles/leader.dir/rule: + cd /Users/pfontana/Documents/GradSchoolClasses/CSDSvn/pfontana/Research/Cleaveland/Code/github_pestimed/TimeSolver && $(MAKE) -f CMakeFiles/Makefile2 examples/ExampleGenerators/CMakeFiles/leader.dir/rule +.PHONY : examples/ExampleGenerators/CMakeFiles/leader.dir/rule + +# Convenience name for target. +leader: examples/ExampleGenerators/CMakeFiles/leader.dir/rule + +.PHONY : leader + +# fast build rule for target. +leader/fast: + cd /Users/pfontana/Documents/GradSchoolClasses/CSDSvn/pfontana/Research/Cleaveland/Code/github_pestimed/TimeSolver && $(MAKE) -f examples/ExampleGenerators/CMakeFiles/leader.dir/build.make examples/ExampleGenerators/CMakeFiles/leader.dir/build +.PHONY : leader/fast + +# Convenience name for target. +examples/ExampleGenerators/CMakeFiles/fischer.dir/rule: + cd /Users/pfontana/Documents/GradSchoolClasses/CSDSvn/pfontana/Research/Cleaveland/Code/github_pestimed/TimeSolver && $(MAKE) -f CMakeFiles/Makefile2 examples/ExampleGenerators/CMakeFiles/fischer.dir/rule +.PHONY : examples/ExampleGenerators/CMakeFiles/fischer.dir/rule + +# Convenience name for target. +fischer: examples/ExampleGenerators/CMakeFiles/fischer.dir/rule + +.PHONY : fischer + +# fast build rule for target. +fischer/fast: + cd /Users/pfontana/Documents/GradSchoolClasses/CSDSvn/pfontana/Research/Cleaveland/Code/github_pestimed/TimeSolver && $(MAKE) -f examples/ExampleGenerators/CMakeFiles/fischer.dir/build.make examples/ExampleGenerators/CMakeFiles/fischer.dir/build +.PHONY : fischer/fast + +# Convenience name for target. +examples/ExampleGenerators/CMakeFiles/pathos.dir/rule: + cd /Users/pfontana/Documents/GradSchoolClasses/CSDSvn/pfontana/Research/Cleaveland/Code/github_pestimed/TimeSolver && $(MAKE) -f CMakeFiles/Makefile2 examples/ExampleGenerators/CMakeFiles/pathos.dir/rule +.PHONY : examples/ExampleGenerators/CMakeFiles/pathos.dir/rule + +# Convenience name for target. +pathos: examples/ExampleGenerators/CMakeFiles/pathos.dir/rule + +.PHONY : pathos + +# fast build rule for target. +pathos/fast: + cd /Users/pfontana/Documents/GradSchoolClasses/CSDSvn/pfontana/Research/Cleaveland/Code/github_pestimed/TimeSolver && $(MAKE) -f examples/ExampleGenerators/CMakeFiles/pathos.dir/build.make examples/ExampleGenerators/CMakeFiles/pathos.dir/build +.PHONY : pathos/fast + +# Convenience name for target. +examples/ExampleGenerators/CMakeFiles/fddi.dir/rule: + cd /Users/pfontana/Documents/GradSchoolClasses/CSDSvn/pfontana/Research/Cleaveland/Code/github_pestimed/TimeSolver && $(MAKE) -f CMakeFiles/Makefile2 examples/ExampleGenerators/CMakeFiles/fddi.dir/rule +.PHONY : examples/ExampleGenerators/CMakeFiles/fddi.dir/rule + +# Convenience name for target. +fddi: examples/ExampleGenerators/CMakeFiles/fddi.dir/rule + +.PHONY : fddi + +# fast build rule for target. +fddi/fast: + cd /Users/pfontana/Documents/GradSchoolClasses/CSDSvn/pfontana/Research/Cleaveland/Code/github_pestimed/TimeSolver && $(MAKE) -f examples/ExampleGenerators/CMakeFiles/fddi.dir/build.make examples/ExampleGenerators/CMakeFiles/fddi.dir/build +.PHONY : fddi/fast + +# Convenience name for target. +examples/ExampleGenerators/CMakeFiles/csma.dir/rule: + cd /Users/pfontana/Documents/GradSchoolClasses/CSDSvn/pfontana/Research/Cleaveland/Code/github_pestimed/TimeSolver && $(MAKE) -f CMakeFiles/Makefile2 examples/ExampleGenerators/CMakeFiles/csma.dir/rule +.PHONY : examples/ExampleGenerators/CMakeFiles/csma.dir/rule + +# Convenience name for target. +csma: examples/ExampleGenerators/CMakeFiles/csma.dir/rule + +.PHONY : csma + +# fast build rule for target. +csma/fast: + cd /Users/pfontana/Documents/GradSchoolClasses/CSDSvn/pfontana/Research/Cleaveland/Code/github_pestimed/TimeSolver && $(MAKE) -f examples/ExampleGenerators/CMakeFiles/csma.dir/build.make examples/ExampleGenerators/CMakeFiles/csma.dir/build +.PHONY : csma/fast + +csma.o: csma.cc.o + +.PHONY : csma.o + +# target to build an object file +csma.cc.o: + cd /Users/pfontana/Documents/GradSchoolClasses/CSDSvn/pfontana/Research/Cleaveland/Code/github_pestimed/TimeSolver && $(MAKE) -f examples/ExampleGenerators/CMakeFiles/csma.dir/build.make examples/ExampleGenerators/CMakeFiles/csma.dir/csma.cc.o +.PHONY : csma.cc.o + +csma.i: csma.cc.i + +.PHONY : csma.i + +# target to preprocess a source file +csma.cc.i: + cd /Users/pfontana/Documents/GradSchoolClasses/CSDSvn/pfontana/Research/Cleaveland/Code/github_pestimed/TimeSolver && $(MAKE) -f examples/ExampleGenerators/CMakeFiles/csma.dir/build.make examples/ExampleGenerators/CMakeFiles/csma.dir/csma.cc.i +.PHONY : csma.cc.i + +csma.s: csma.cc.s + +.PHONY : csma.s + +# target to generate assembly for a file +csma.cc.s: + cd /Users/pfontana/Documents/GradSchoolClasses/CSDSvn/pfontana/Research/Cleaveland/Code/github_pestimed/TimeSolver && $(MAKE) -f examples/ExampleGenerators/CMakeFiles/csma.dir/build.make examples/ExampleGenerators/CMakeFiles/csma.dir/csma.cc.s +.PHONY : csma.cc.s + +fddi.o: fddi.cc.o + +.PHONY : fddi.o + +# target to build an object file +fddi.cc.o: + cd /Users/pfontana/Documents/GradSchoolClasses/CSDSvn/pfontana/Research/Cleaveland/Code/github_pestimed/TimeSolver && $(MAKE) -f examples/ExampleGenerators/CMakeFiles/fddi.dir/build.make examples/ExampleGenerators/CMakeFiles/fddi.dir/fddi.cc.o +.PHONY : fddi.cc.o + +fddi.i: fddi.cc.i + +.PHONY : fddi.i + +# target to preprocess a source file +fddi.cc.i: + cd /Users/pfontana/Documents/GradSchoolClasses/CSDSvn/pfontana/Research/Cleaveland/Code/github_pestimed/TimeSolver && $(MAKE) -f examples/ExampleGenerators/CMakeFiles/fddi.dir/build.make examples/ExampleGenerators/CMakeFiles/fddi.dir/fddi.cc.i +.PHONY : fddi.cc.i + +fddi.s: fddi.cc.s + +.PHONY : fddi.s + +# target to generate assembly for a file +fddi.cc.s: + cd /Users/pfontana/Documents/GradSchoolClasses/CSDSvn/pfontana/Research/Cleaveland/Code/github_pestimed/TimeSolver && $(MAKE) -f examples/ExampleGenerators/CMakeFiles/fddi.dir/build.make examples/ExampleGenerators/CMakeFiles/fddi.dir/fddi.cc.s +.PHONY : fddi.cc.s + +fischer.o: fischer.cc.o + +.PHONY : fischer.o + +# target to build an object file +fischer.cc.o: + cd /Users/pfontana/Documents/GradSchoolClasses/CSDSvn/pfontana/Research/Cleaveland/Code/github_pestimed/TimeSolver && $(MAKE) -f examples/ExampleGenerators/CMakeFiles/fischer.dir/build.make examples/ExampleGenerators/CMakeFiles/fischer.dir/fischer.cc.o +.PHONY : fischer.cc.o + +fischer.i: fischer.cc.i + +.PHONY : fischer.i + +# target to preprocess a source file +fischer.cc.i: + cd /Users/pfontana/Documents/GradSchoolClasses/CSDSvn/pfontana/Research/Cleaveland/Code/github_pestimed/TimeSolver && $(MAKE) -f examples/ExampleGenerators/CMakeFiles/fischer.dir/build.make examples/ExampleGenerators/CMakeFiles/fischer.dir/fischer.cc.i +.PHONY : fischer.cc.i + +fischer.s: fischer.cc.s + +.PHONY : fischer.s + +# target to generate assembly for a file +fischer.cc.s: + cd /Users/pfontana/Documents/GradSchoolClasses/CSDSvn/pfontana/Research/Cleaveland/Code/github_pestimed/TimeSolver && $(MAKE) -f examples/ExampleGenerators/CMakeFiles/fischer.dir/build.make examples/ExampleGenerators/CMakeFiles/fischer.dir/fischer.cc.s +.PHONY : fischer.cc.s + +grc.o: grc.cc.o + +.PHONY : grc.o + +# target to build an object file +grc.cc.o: + cd /Users/pfontana/Documents/GradSchoolClasses/CSDSvn/pfontana/Research/Cleaveland/Code/github_pestimed/TimeSolver && $(MAKE) -f examples/ExampleGenerators/CMakeFiles/grc.dir/build.make examples/ExampleGenerators/CMakeFiles/grc.dir/grc.cc.o +.PHONY : grc.cc.o + +grc.i: grc.cc.i + +.PHONY : grc.i + +# target to preprocess a source file +grc.cc.i: + cd /Users/pfontana/Documents/GradSchoolClasses/CSDSvn/pfontana/Research/Cleaveland/Code/github_pestimed/TimeSolver && $(MAKE) -f examples/ExampleGenerators/CMakeFiles/grc.dir/build.make examples/ExampleGenerators/CMakeFiles/grc.dir/grc.cc.i +.PHONY : grc.cc.i + +grc.s: grc.cc.s + +.PHONY : grc.s + +# target to generate assembly for a file +grc.cc.s: + cd /Users/pfontana/Documents/GradSchoolClasses/CSDSvn/pfontana/Research/Cleaveland/Code/github_pestimed/TimeSolver && $(MAKE) -f examples/ExampleGenerators/CMakeFiles/grc.dir/build.make examples/ExampleGenerators/CMakeFiles/grc.dir/grc.cc.s +.PHONY : grc.cc.s + +leader.o: leader.cc.o + +.PHONY : leader.o + +# target to build an object file +leader.cc.o: + cd /Users/pfontana/Documents/GradSchoolClasses/CSDSvn/pfontana/Research/Cleaveland/Code/github_pestimed/TimeSolver && $(MAKE) -f examples/ExampleGenerators/CMakeFiles/leader.dir/build.make examples/ExampleGenerators/CMakeFiles/leader.dir/leader.cc.o +.PHONY : leader.cc.o + +leader.i: leader.cc.i + +.PHONY : leader.i + +# target to preprocess a source file +leader.cc.i: + cd /Users/pfontana/Documents/GradSchoolClasses/CSDSvn/pfontana/Research/Cleaveland/Code/github_pestimed/TimeSolver && $(MAKE) -f examples/ExampleGenerators/CMakeFiles/leader.dir/build.make examples/ExampleGenerators/CMakeFiles/leader.dir/leader.cc.i +.PHONY : leader.cc.i + +leader.s: leader.cc.s + +.PHONY : leader.s + +# target to generate assembly for a file +leader.cc.s: + cd /Users/pfontana/Documents/GradSchoolClasses/CSDSvn/pfontana/Research/Cleaveland/Code/github_pestimed/TimeSolver && $(MAKE) -f examples/ExampleGenerators/CMakeFiles/leader.dir/build.make examples/ExampleGenerators/CMakeFiles/leader.dir/leader.cc.s +.PHONY : leader.cc.s + +pathos.o: pathos.cc.o + +.PHONY : pathos.o + +# target to build an object file +pathos.cc.o: + cd /Users/pfontana/Documents/GradSchoolClasses/CSDSvn/pfontana/Research/Cleaveland/Code/github_pestimed/TimeSolver && $(MAKE) -f examples/ExampleGenerators/CMakeFiles/pathos.dir/build.make examples/ExampleGenerators/CMakeFiles/pathos.dir/pathos.cc.o +.PHONY : pathos.cc.o + +pathos.i: pathos.cc.i + +.PHONY : pathos.i + +# target to preprocess a source file +pathos.cc.i: + cd /Users/pfontana/Documents/GradSchoolClasses/CSDSvn/pfontana/Research/Cleaveland/Code/github_pestimed/TimeSolver && $(MAKE) -f examples/ExampleGenerators/CMakeFiles/pathos.dir/build.make examples/ExampleGenerators/CMakeFiles/pathos.dir/pathos.cc.i +.PHONY : pathos.cc.i + +pathos.s: pathos.cc.s + +.PHONY : pathos.s + +# target to generate assembly for a file +pathos.cc.s: + cd /Users/pfontana/Documents/GradSchoolClasses/CSDSvn/pfontana/Research/Cleaveland/Code/github_pestimed/TimeSolver && $(MAKE) -f examples/ExampleGenerators/CMakeFiles/pathos.dir/build.make examples/ExampleGenerators/CMakeFiles/pathos.dir/pathos.cc.s +.PHONY : pathos.cc.s + +# Help Target +help: + @echo "The following are some of the valid targets for this Makefile:" + @echo "... all (the default if no target is provided)" + @echo "... clean" + @echo "... depend" + @echo "... install/strip" + @echo "... install/local" + @echo "... rebuild_cache" + @echo "... edit_cache" + @echo "... grc" + @echo "... test" + @echo "... leader" + @echo "... fischer" + @echo "... list_install_components" + @echo "... install" + @echo "... pathos" + @echo "... fddi" + @echo "... csma" + @echo "... csma.o" + @echo "... csma.i" + @echo "... csma.s" + @echo "... fddi.o" + @echo "... fddi.i" + @echo "... fddi.s" + @echo "... fischer.o" + @echo "... fischer.i" + @echo "... fischer.s" + @echo "... grc.o" + @echo "... grc.i" + @echo "... grc.s" + @echo "... leader.o" + @echo "... leader.i" + @echo "... leader.s" + @echo "... pathos.o" + @echo "... pathos.i" + @echo "... pathos.s" +.PHONY : help + + + +#============================================================================= +# Special targets to cleanup operation of make. + +# Special rule to run CMake to check the build system integrity. +# No rule that depends on this can have commands that come from listfiles +# because they might be regenerated. +cmake_check_build_system: + cd /Users/pfontana/Documents/GradSchoolClasses/CSDSvn/pfontana/Research/Cleaveland/Code/github_pestimed/TimeSolver && $(CMAKE_COMMAND) -S$(CMAKE_SOURCE_DIR) -B$(CMAKE_BINARY_DIR) --check-build-system CMakeFiles/Makefile.cmake 0 +.PHONY : cmake_check_build_system diff --git a/pes.timed/ExprNode.cc b/pes.timed/ExprNode.cc index f3d4b29..27cc636 100644 --- a/pes.timed/ExprNode.cc +++ b/pes.timed/ExprNode.cc @@ -397,3 +397,371 @@ void print_ExprNodeTrans(const ExprNode* const e, std::ostream& os) { } } } + +/** Prints out the expression to the desired output stream, labeling + * the expression with its opType. The typical output stream is cout. + * @param e (*) The expression to print out. + * @param os (&) The type of output stream to print the output to. + * @return None */ +void ExprNode::printExamined(std::ostream& os) +{ + + if(!(getExaminedDuringProof())) { + cout << "**u**"; + // Note: mark this formula as being bypassed + //e->setBypassedDuringProof(true); + } + switch (getOpType()){ + case PREDICATE: + os << getPredicate() ; + break; + case FORALL: + os << "FORALL.["; + getQuant()->printExamined(os); + os << "]"; + break; + case EXISTS: + os << "EXISTS.["; + getQuant()->printExamined(os); + os << "]"; + break; + case FORALL_REL: + os << "FORALLREL.("; + getLeft()->printExamined(os); + os << ")["; + getRight()->printExamined(os); + os << "]"; + break; + case EXISTS_REL: + os << "EXISTSREL.("; + getLeft()->printExamined(os); + os << ")["; + getRight()->printExamined(os); + os << "]"; + break; + case ALLACT: + os << "ALLACT.["; + getQuant()->printExamined(os); + os << "]"; + break; + case EXISTACT: + os << "EXISTACT.["; + getQuant()->printExamined(os); + os << "]"; + break; + case AND: + os << "("; + getLeft()->printExamined(os); + os << " AND "; + getRight()->printExamined(os); + os << ")"; + break; + case OR: + cout << "("; + getLeft()->printExamined(os); + os << " OR "; + getRight()->printExamined(os); + cout << ")"; + break; + case OR_SIMPLE: + cout << "("; + getLeft()->printExamined(os); + os << " OR_S "; + getRight()->printExamined(os); + cout << ")"; + break; + case IMPLY: + os << "-(-"; + getLeft()->printExamined(os); + os << " IMPLY "; + getRight()->printExamined(os); + os << "-)-"; + break; + case RESET: + getExpr()->printExamined(os); + getClockSet()->print(os); + break; + case REPLACE: + getExpr()->printExamined(os); + os << "p" << (getAtomic()); + os << ":="; + os << getIntVal(); + break; + case CONSTRAINT: + dbm()->print_constraint(os); + break; + case ATOMIC: + os << "p" << (getAtomic()); + os << "=="; + os << getIntVal(); + break; + case ATOMIC_NOT: + os << "p" << (getAtomic()); + os << "!="; + os << getIntVal(); + break; + case ATOMIC_LT: + os << "p" << (getAtomic()); + os << "<"; + os << getIntVal(); + break; + case ATOMIC_GT: + os << "p" << (getAtomic()); + os << ">"; + os << getIntVal(); + break; + case ATOMIC_LE: + os << "p" << (getAtomic()); + os << "<="; + os << getIntVal(); + break; + case ATOMIC_GE: + os << "p" << (getAtomic()); + os << ">="; + os << getIntVal(); + break; + case BOOL: + os << ((getBool())? "TRUE" : "FALSE"); + break; + case SUBLIST: + getExpr()->printExamined(os); + getSublist()->print(os); + break; + case ASSIGN: + getExpr()->printExamined(os); + os << "["; + os << "x" << (getcX()); + os << "=="; + os << "x" << (getcY()); + os << "]"; + break; + case ABLEWAITINF: + os << "AbleWaitInf"; + break; + case UNABLEWAITINF: + os << "UnableWaitInf"; + break; + } + if(!(getExaminedDuringProof())) { + cout << "**u**"; + } + + +} + +/** Prints out the expression to the desired output stream, labeling + * the expression with its opType. The typical output stream is cout. + * @param e (*) The expression to print out. + * @param os (&) The type of output stream to print the output to. + * param proovVal true if the sequent was proven valid; false otherwise. + * @return None */ + void ExprNode::printDetectVacuous(std::ostream& os, bool proofVal) + { + if(!(getExaminedDuringProof())) { + cout << "*--v--*"; + } + switch (getOpType()){ + case PREDICATE: + os << getPredicate() ; + break; + case FORALL: + os << "FORALL.["; + getQuant()->printDetectVacuous(os, proofVal); + os << "]"; + break; + case EXISTS: + os << "EXISTS.["; + getQuant()->printDetectVacuous(os, proofVal); + os << "]"; + break; + case FORALL_REL: + os << "FORALLREL.("; + getLeft()->printDetectVacuous(os, proofVal); + os << ")["; + getRight()->printDetectVacuous(os, proofVal); + os << "]"; + break; + case EXISTS_REL: + os << "EXISTSREL.("; + getLeft()->printDetectVacuous(os, proofVal); + os << ")["; + getRight()->printDetectVacuous(os, proofVal); + os << "]"; + break; + case ALLACT: + os << "ALLACT.["; + getQuant()->printDetectVacuous(os, proofVal); + os << "]"; + break; + case EXISTACT: + os << "EXISTACT.["; + getQuant()->printDetectVacuous(os, proofVal); + os << "]"; + break; + case AND: + cout << "("; + if(proofVal) { + getLeft()->printDetectVacuous(os, proofVal); + os << " AND "; + getRight()->printDetectVacuous(os, proofVal); + } + else { + if(getLeft()->getExaminedDuringProof() && + !(getRight()->getBypassedDuringProof()) && !(getRight()->getValidDuringProof()) ) { + cout << "*--v--*"; + } + getLeft()->printDetectVacuous(os, proofVal); + if(getLeft()->getExaminedDuringProof() && + !(getRight()->getBypassedDuringProof()) && !(getRight()->getValidDuringProof()) ) { + cout << "*--v--*"; + } + os << " AND "; + if(getRight()->getExaminedDuringProof() && + !(getLeft()->getBypassedDuringProof()) && !(getLeft()->getValidDuringProof()) ) { + cout << "*--v--*"; + } + getRight()->printDetectVacuous(os, proofVal); + if(getRight()->getExaminedDuringProof() && + !(getLeft()->getBypassedDuringProof()) && !(getLeft()->getValidDuringProof()) ) { + cout << "*--v--*"; + } + } + cout << ")"; + break; + case OR: + cout << "("; + if(proofVal) { + if(getLeft()->getExaminedDuringProof() && + !(getRight()->getBypassedDuringProof()) && !(getRight()->getInvalidDuringProof()) ) { + cout << "*--v--*"; + } + getLeft()->printDetectVacuous(os, proofVal); + if(getLeft()->getExaminedDuringProof() && + !(getRight()->getBypassedDuringProof()) && !(getRight()->getInvalidDuringProof()) ) { + cout << "*--v--*"; + } + os << " OR "; + if(getRight()->getExaminedDuringProof() && + !(getLeft()->getBypassedDuringProof()) && !(getLeft()->getInvalidDuringProof()) ) { + cout << "*--v--*"; + } + getRight()->printDetectVacuous(os, proofVal); + if(getRight()->getExaminedDuringProof() && + !(getLeft()->getBypassedDuringProof()) && !(getLeft()->getInvalidDuringProof()) ) { + cout << "*--v--*"; + } + } + else { + getLeft()->printDetectVacuous(os, proofVal); + os << " OR "; + getRight()->printDetectVacuous(os, proofVal); + } + cout << ")"; + break; + case OR_SIMPLE: + cout << "("; + if(proofVal) { + if(getLeft()->getExaminedDuringProof() && + !(getRight()->getBypassedDuringProof()) && !(getRight()->getInvalidDuringProof()) ) { + cout << "*--v--*"; + } + getLeft()->printDetectVacuous(os, proofVal); + if(getLeft()->getExaminedDuringProof() && + !(getRight()->getBypassedDuringProof()) && !(getRight()->getInvalidDuringProof()) ) { + cout << "*--v--*"; + } + os << " OR_S "; + if(getRight()->getExaminedDuringProof() && + !(getLeft()->getBypassedDuringProof()) && !(getLeft()->getInvalidDuringProof()) ) { + cout << "*--v--*"; + } + getRight()->printDetectVacuous(os, proofVal); + if(getRight()->getExaminedDuringProof() && + !(getLeft()->getBypassedDuringProof()) && !(getLeft()->getInvalidDuringProof()) ) { + cout << "*--v--*"; + } + } + else { + getLeft()->printDetectVacuous(os, proofVal); + os << " OR_S "; + getRight()->printDetectVacuous(os, proofVal); + } + cout << ")"; + break; + case IMPLY: + os << "-(-"; + getLeft()->printDetectVacuous(os, proofVal); + os << " IMPLY "; + getRight()->printDetectVacuous(os, proofVal); + os << "-)-"; + break; + case RESET: + getExpr()->printDetectVacuous(os, proofVal); + getClockSet()->print(os); + break; + case REPLACE: + getExpr()->printDetectVacuous(os, proofVal); + os << "p" << (getAtomic()); + os << ":="; + os << getIntVal(); + break; + case CONSTRAINT: + dbm()->print_constraint(os); + break; + case ATOMIC: + os << "p" << (getAtomic()); + os << "=="; + os << getIntVal(); + break; + case ATOMIC_NOT: + os << "p" << (getAtomic()); + os << "!="; + os << getIntVal(); + break; + case ATOMIC_LT: + os << "p" << (getAtomic()); + os << "<"; + os << getIntVal(); + break; + case ATOMIC_GT: + os << "p" << (getAtomic()); + os << ">"; + os << getIntVal(); + break; + case ATOMIC_LE: + os << "p" << (getAtomic()); + os << "<="; + os << getIntVal(); + break; + case ATOMIC_GE: + os << "p" << (getAtomic()); + os << ">="; + os << getIntVal(); + break; + case BOOL: + os << ((getBool())? "TRUE" : "FALSE"); + break; + case SUBLIST: + getExpr()->printDetectVacuous(os, proofVal); + getSublist()->print(os); + break; + case ASSIGN: + getExpr()->printDetectVacuous(os, proofVal); + os << "["; + os << "x" << (getcX()); + os << "=="; + os << "x" << (getcY()); + os << "]"; + break; + case ABLEWAITINF: + os << "AbleWaitInf"; + break; + case UNABLEWAITINF: + os << "UnableWaitInf"; + break; + } + if(!(getExaminedDuringProof())) { + cout << "*--v--*"; + } + + } diff --git a/pes.timed/ExprNode.hh b/pes.timed/ExprNode.hh index ee8247a..b7baecc 100644 --- a/pes.timed/ExprNode.hh +++ b/pes.timed/ExprNode.hh @@ -228,6 +228,14 @@ public: predicate = nullptr; subst = nullptr; assert(q != nullptr); + examinedDuringProof = false; + bypassedDuringProof = false; + validDuringProof = false; + invalidDuringProof = false; + validReqDuringProof = false; + invalidReqDuringProof = false; + justRequiredValid = false; + justRequiredInvalid = false; } /** Constructor for two-children expressions with @@ -248,6 +256,14 @@ public: subst = nullptr; assert(l != nullptr); assert(r != nullptr); + examinedDuringProof = false; + bypassedDuringProof = false; + validDuringProof = false; + invalidDuringProof = false; + validReqDuringProof = false; + invalidReqDuringProof = false; + justRequiredValid = false; + justRequiredInvalid = false; } /** Constructor for a clock constraint expression with optype = {CONSTRAINT}. @@ -268,6 +284,14 @@ public: constraint = c; m_clock_set = nullptr; subst = nullptr; + examinedDuringProof = false; + bypassedDuringProof = false; + validDuringProof = false; + invalidDuringProof = false; + validReqDuringProof = false; + invalidReqDuringProof = false; + justRequiredValid = false; + justRequiredInvalid = false; } /** Constructor for a boolean expression of true or false @@ -290,6 +314,14 @@ public: constraint = nullptr; m_clock_set = nullptr; subst = nullptr; + examinedDuringProof = false; + bypassedDuringProof = false; + validDuringProof = false; + invalidDuringProof = false; + validReqDuringProof = false; + invalidReqDuringProof = false; + justRequiredValid = false; + justRequiredInvalid = false; } /** Constructor for atomic (state value) expressions with @@ -317,6 +349,14 @@ public: subst = nullptr; m_clock_set = nullptr; constraint = nullptr; + examinedDuringProof = false; + bypassedDuringProof = false; + validDuringProof = false; + invalidDuringProof = false; + validReqDuringProof = false; + invalidReqDuringProof = false; + justRequiredValid = false; + justRequiredInvalid = false; } /** Constructor for invariant sub-expressions with opType = {ATOMIC}. @@ -350,6 +390,14 @@ public: predicate = nullptr; m_clock_set = nullptr; subst = nullptr; + examinedDuringProof = false; + bypassedDuringProof = false; + validDuringProof = false; + invalidDuringProof = false; + validReqDuringProof = false; + invalidReqDuringProof = false; + justRequiredValid = false; + justRequiredInvalid = false; } /** Constructor for predicate variable expressions with opType = {PREDICATE}. @@ -372,6 +420,14 @@ public: m_clock_set = nullptr; subst = nullptr; constraint = nullptr; + examinedDuringProof = false; + bypassedDuringProof = false; + validDuringProof = false; + invalidDuringProof = false; + validReqDuringProof = false; + invalidReqDuringProof = false; + justRequiredValid = false; + justRequiredInvalid = false; } /** Constructor for clock set expressions with opType = {RESET}. These @@ -391,6 +447,14 @@ public: predicate = nullptr; constraint = nullptr; subst = nullptr; + examinedDuringProof = false; + bypassedDuringProof = false; + validDuringProof = false; + invalidDuringProof = false; + validReqDuringProof = false; + invalidReqDuringProof = false; + justRequiredValid = false; + justRequiredInvalid = false; } /** Constructor for sublist expressions, representing a change of @@ -413,6 +477,14 @@ public: predicate = nullptr; m_clock_set = nullptr; constraint = nullptr; + examinedDuringProof = false; + bypassedDuringProof = false; + validDuringProof = false; + invalidDuringProof = false; + validReqDuringProof = false; + invalidReqDuringProof = false; + justRequiredValid = false; + justRequiredInvalid = false; } /** Constructor for assignment and replacement expressions with @@ -444,6 +516,14 @@ public: m_clock_set = nullptr; constraint = nullptr; subst = nullptr; + examinedDuringProof = false; + bypassedDuringProof = false; + validDuringProof = false; + invalidDuringProof = false; + validReqDuringProof = false; + invalidReqDuringProof = false; + justRequiredValid = false; + justRequiredInvalid = false; } /** Copy Constructor. This is used when an expression needs to be duplicated @@ -524,6 +604,34 @@ public: /* Note: since predicates are shallow-copied, they are not deleted * here. */ } + + /* Note: subformulas are trickier since in circularity */ + void clearValidReq() { + if(validReqDuringProof && justRequiredValid) { + //validReqDuringProof = false; + //justRequiredValid = false; + } + if(left != NULL){ + left->clearValidReq(); + } + if(right != NULL){ + right->clearValidReq(); + } + } + + /* Note: subformulas are trickier since in circularity */ + void clearInvalidReq() { + if(invalidReqDuringProof && justRequiredInvalid) { + //invalidReqDuringProof = false; + //justRequiredInvalid = false; + } + if(left != NULL){ + left->clearInvalidReq(); + } + if(right != NULL){ + right->clearInvalidReq(); + } + } /** Returns the opType of the expression, which labels/categorizes * the expression. @@ -539,16 +647,18 @@ public: ExprNode* getQuant() const { return left; } /** Returns the left child of the ExprNode. + * This is non constant so the prover can mark vacuity variables. * @note This does the same thing as getQuant(), but tends to be used * for expressions with two (left and right) children. * @return The reference to the left (or single) child of that expression. * @see The Constructor(s) comments for more information. */ - const ExprNode* getLeft() const { return left; } + ExprNode* getLeft() const { return left; } /** Returns the right (or second) child of the expression. + * This is non constant so the prover can mark vacuity variables. * @return The reference to the right (or second) child of that expression. * @see The Constructor(s) comments for more information. */ - const ExprNode* getRight() const { return right; } + ExprNode* getRight() const { return right; } /** Returns the clock constraint (DBM representation) of the expression. * @return The reference to the DBM representing the clock constraints. @@ -639,6 +749,13 @@ public: * @note This does the same thing as getBool(). It is used differently. * @see The Constructor(s) comments for more information. */ bool is_gfp() const { return b; } + + /** Returns the parity of the expression: true = gfp, false = lfp. + * @return The parity (as a boolean) of the + * expression: true = gfp, false = lfp. + * @note This does the same thing as getBool(). It is used differently. + * @see The Constructor(s) comments for more information. */ + bool get_Parity() const {return b;} /** Returns the integer representing the block number of the expression. * This function is used for PREDICATE expressions. @@ -719,6 +836,115 @@ public: * @param destR (*) the (right) child expression * @return None. */ void setExprDestRight(ExprNode* destR) { right = destR; } + + /** This returns the value of the boolean + * indicating whether this expression was examined by the prover. + * @return true: if the expression was examined; false: otherwise */ + bool getExaminedDuringProof() { + return examinedDuringProof; + } + + /** This returns the value of the boolean + * indicating whether this expression was bypassed by the prover. + * @return true: if the expression was examined; false: otherwise */ + bool getBypassedDuringProof() { + return bypassedDuringProof; + } + + /** This returns the value of the boolean + * indicating whether this expression was shown valid by the prover + * for any left hand sequent. + * @return true: if the expression is valid for some state; + * false: otherwise */ + bool getValidDuringProof() { + return validDuringProof; + } + + /** This returns the value of the boolean + * indicating whether this expression was shown invalid by the prover + * for any left hand sequent. + * @return true: if the expression is invalid for some state; + * false: otherwise */ + bool getInvalidDuringProof() { + return invalidDuringProof; + } + + /** This returns the value of the boolean + * indicating whether this expression was shown valid by the prover + * and was needed for any left hand sequent. + * @return true: if the expression is valid for some state; + * false: otherwise */ + bool getValidReqDuringProof() { + return validReqDuringProof; + } + + /** This returns the value of the boolean + * indicating whether this expression was shown invalid by the prover + * and was needed for any left hand sequent. + * @return true: if the expression is invalid for some state; + * false: otherwise */ + bool getInvalidReqDuringProof() { + return invalidReqDuringProof; + } + + bool getJustRequiredValid() { + return justRequiredValid; + } + + bool getJustRequiredInvalid() { + return justRequiredInvalid; + } + + + /** Records whether this expression was examined by + * the PES prover. + * @param newVal the boolean value to record. */ + void setExaminedDuringProof(bool newVal) { + examinedDuringProof = newVal; + } + + /** Records whether this expression was bypassed by + * the PES prover. + * @param newVal the boolean value to record. */ + void setBypassedDuringProof(bool newVal) { + bypassedDuringProof = newVal; + } + + /** Records whether this expression was shown valid + * for some left hand sequent. + * @param newVal the boolean value to record. */ + void setValidDuringProof(bool newVal) { + validDuringProof = newVal; + } + + /** Records whether this expression was shown invalid + * for some left hand sequent. + * @param newVal the boolean value to record. */ + void setInvalidDuringProof(bool newVal) { + invalidDuringProof = newVal; + } + + /** Records whether this expression was shown valid + * and needed for that branch for some left hand sequent. + * @param newVal the boolean value to record. */ + void setValidReqDuringProof(bool newVal) { + validReqDuringProof = newVal; + } + + /** Records whether this expression was shown invalid + * and needed for that branch for some left hand sequent. + * @param newVal the boolean value to record. */ + void setInvalidReqDuringProof(bool newVal) { + invalidReqDuringProof = newVal; + } + + void setJustRequiredValid(bool newVal) { + justRequiredValid = newVal; + } + + void setJustRequiredInvalid(bool newVal) { + justRequiredInvalid = newVal; + } protected: /* Note: The data variables here are used as a "quasi-union", @@ -753,6 +979,31 @@ protected: * child expression. The SubstList is often the "state", * giving values to propositions (or control values). Possibly empty. */ SubstList* subst; + + /** This boolean is true if the PES prover examined this subformula + * (expression) for some left hand sequent. */ + bool examinedDuringProof; + /** This boolean is true if the PES prover found this expression + * valid for any left hand sequent. */ + bool validDuringProof; + /** This boolean is true if the PES prover found this expression + * invalid for any left hand sequent. This is also true + * when a split or is used, since the subformula is only + * true for some of the states in the sequent. */ + bool invalidDuringProof; + /** This boolean is true if the PES prover bypassed this subformula + * (expression) for some left hand sequent. */ + bool bypassedDuringProof; + + /** This boolean is true if the PES prover found this expression + * valid and requierd as valid for any left hand sequent. */ + bool validReqDuringProof; + /** This boolean is true if the PES prover found this expression + * invalid and required invalid for any left hand sequent.*/ + bool invalidReqDuringProof; + + bool justRequiredValid; + bool justRequiredInvalid; /** The "opcode" or Type ID of the Expression Node. * This type determines @@ -798,6 +1049,21 @@ public: * @param os (&) The type of output stream to print the output to. * @return None */ void print(std::ostream& os) const; + + /** Prints out the expression to the desired output stream, labeling + * the expression with its opType. The typical output stream is cout. + * @param e (*) The expression to print out. + * @param os (&) The type of output stream to print the output to. + * @return None */ + void printExamined(std::ostream& os); + + /** Prints out the expression to the desired output stream, labeling + * the expression with its opType. The typical output stream is cout. + * @param e (*) The expression to print out. + * @param os (&) The type of output stream to print the output to. + * param proovVal true if the sequent was proven valid; false otherwise. + * @return None */ + void printDetectVacuous(std::ostream& os, bool proofVal); }; /** Overload for streaming ExprNode to output stream */ diff --git a/pes.timed/proof.hh b/pes.timed/proof.hh index 161918d..88b27a2 100644 --- a/pes.timed/proof.hh +++ b/pes.timed/proof.hh @@ -81,7 +81,7 @@ public: * is included in the resulting placeholder. */ bool do_proof_init(pes& p, DBMList* placeholder = nullptr) { - const ExprNode* start_pred = p.lookup_predicate(p.start_predicate()); + ExprNode* start_pred = p.lookup_predicate(p.start_predicate()); if (placeholder == nullptr) { @@ -114,7 +114,7 @@ protected: __attribute__((flatten)) bool do_proof(const SubstList& discrete_state, const DBM& zone, - const ExprNode& formula) { + ExprNode& formula) { assert(zone.isInCf()); bool result = false; if (cpplogEnabled(cpplogging::debug)) { @@ -122,6 +122,10 @@ protected: formula.getOpType()); } ++step; + + if(!options.allVacuity) { + formula.setExaminedDuringProof(true); + } switch (formula.getOpType()) { case PREDICATE: { @@ -225,6 +229,14 @@ protected: break; } } + if(!options.allVacuity) { + if(result) { + //formula.getRight()->setValidDuringProof(true); + } + else { + //formula.getRight()->setInvalidDuringProof(true); + } + } --step; return result; } @@ -248,7 +260,7 @@ protected: * and the return value. */ __attribute__((flatten)) void do_proof_place(const SubstList& discrete_state, const DBM& zone, DBMList* place, - const ExprNode& formula) { + ExprNode& formula) { /* do_proof_place() written by Peter Fontana, needed for support * of EXISTS Quantifiers. */ assert(zone.isInCf()); @@ -258,6 +270,10 @@ protected: print_sequent_place(std::cerr, step, false, zone, *place, formula, discrete_state, formula.getOpType()); } + + if(!options.allVacuity) { + formula.setExaminedDuringProof(true); + } ++step; switch (formula.getOpType()) { @@ -362,102 +378,110 @@ protected: break; } } + if(!options.allVacuity) { + if( (place!=NULL) & !(place->emptiness())) { + //formula.getRight()->setValidDuringProof(true); + } + else { + //formula.getRight()->setInvalidDuringProof(true); + } + } --step; } bool do_proof_predicate(const SubstList& discrete_state, const DBM& zone, - const ExprNode& formula); + ExprNode& formula); bool do_proof_and(const SubstList& discrete_state, const DBM& zone, - const ExprNode& formula); + ExprNode& formula); bool do_proof_or(const SubstList& discrete_state, const DBM& zone, - const ExprNode& formula); + ExprNode& formula); bool do_proof_or_simple(const SubstList& discrete_state, const DBM& zone, - const ExprNode& formula); + ExprNode& formula); bool do_proof_forall(const SubstList& discrete_state, const DBM& zone, - const ExprNode& formula); + ExprNode& formula); bool do_proof_forall_rel(const SubstList& discrete_state, const DBM& zone, - const ExprNode& formula); + ExprNode& formula); bool do_proof_exists(const SubstList& discrete_state, const DBM& zone, - const ExprNode& formula); + ExprNode& formula); bool do_proof_exists_rel(const SubstList& discrete_state, const DBM& zone, - const ExprNode& formula); + ExprNode& formula); bool do_proof_allact(const SubstList& discrete_state, const DBM& zone, - const ExprNode& formula); + ExprNode& formula); bool do_proof_existact(const SubstList& discrete_state, const DBM& zone, - const ExprNode& formula); + ExprNode& formula); bool do_proof_imply(const SubstList& discrete_state, const DBM& zone, - const ExprNode& formula); - bool do_proof_constraint(const DBM& zone, const ExprNode& formula) const; + ExprNode& formula); + bool do_proof_constraint(const DBM& zone, ExprNode& formula) const; bool do_proof_sublist(const SubstList& discrete_state, const DBM& zone, - const ExprNode& formula); + ExprNode& formula); bool do_proof_reset(const SubstList& discrete_state, const DBM& zone, - const ExprNode& formula); + ExprNode& formula); bool do_proof_assign(const SubstList& discrete_state, const DBM& zone, - const ExprNode& formula); + ExprNode& formula); bool do_proof_replace(const SubstList& discrete_state, const DBM& zone, - const ExprNode& formula); + ExprNode& formula); void do_proof_place_predicate(const SubstList& discrete_state, const DBM& zone, DBMList* place, - const ExprNode& formula); + ExprNode& formula); void do_proof_place_and(const SubstList& discrete_state, const DBM& zone, DBMList* place, - const ExprNode& formula); + ExprNode& formula); void do_proof_place_or(const SubstList& discrete_state, const DBM& zone, DBMList* place, - const ExprNode& formula); + ExprNode& formula); void do_proof_place_or_simple(const SubstList& discrete_state, const DBM& zone, DBMList* place, - const ExprNode& formula); + ExprNode& formula); void do_proof_place_forall(const SubstList& discrete_state, const DBM& zone, DBMList* place, - const ExprNode& formula); + ExprNode& formula); void do_proof_place_forall_rel(const SubstList& discrete_state, const DBM& zone, DBMList* place, - const ExprNode& formula); + ExprNode& formula); void do_proof_place_exists(const SubstList& discrete_state, const DBM& zone, DBMList* place, - const ExprNode& formula); + ExprNode& formula); void do_proof_place_exists_rel(const SubstList& discrete_state, const DBM& zone, DBMList* place, - const ExprNode& formula); + ExprNode& formula); void do_proof_place_allact(const SubstList& discrete_state, const DBM& zone, DBMList* place, - const ExprNode& formula); + ExprNode& formula); void do_proof_place_existact(const SubstList& discrete_state, const DBM& zone, DBMList* place, - const ExprNode& formula); + ExprNode& formula); void do_proof_place_imply(const SubstList& discrete_state, const DBM& zone, DBMList* place, - const ExprNode& formula); + ExprNode& formula); void do_proof_place_constraint(const DBM& zone, DBMList* place, - const ExprNode& formula) const; - bool do_proof_place_bool(DBMList* place, const ExprNode& formula) const; + ExprNode& formula) const; + bool do_proof_place_bool(DBMList* place, ExprNode& formula) const; bool do_proof_place_atomic(const SubstList& discrete_state, - DBMList* place, const ExprNode& formula) const; + DBMList* place, ExprNode& formula) const; bool do_proof_place_atomic_not(const SubstList& discrete_state, - DBMList* place, const ExprNode& formula) const; + DBMList* place, ExprNode& formula) const; bool do_proof_place_atomic_lt(const SubstList& discrete_state, - DBMList* place, const ExprNode& formula) const; + DBMList* place, ExprNode& formula) const; bool do_proof_place_atomic_gt(const SubstList& discrete_state, - DBMList* place, const ExprNode& formula) const; + DBMList* place, ExprNode& formula) const; bool do_proof_place_atomic_le(const SubstList& discrete_state, - DBMList* place, const ExprNode& formula) const; + DBMList* place, ExprNode& formula) const; bool do_proof_place_atomic_ge(const SubstList& discrete_state, - DBMList* place, const ExprNode& formula) const; + DBMList* place, ExprNode& formula) const; void do_proof_place_sublist(const SubstList& discrete_state, const DBM& zone, DBMList* place, - const ExprNode& formula); + ExprNode& formula); void do_proof_place_reset(const SubstList& discrete_state, const DBM& zone, DBMList* place, - const ExprNode& formula); + ExprNode& formula); void do_proof_place_assign(const SubstList& discrete_state, const DBM& zone, DBMList* place, - const ExprNode& formula); + ExprNode& formula); void do_proof_place_replace(const SubstList& discrete_state, const DBM& zone, DBMList* place, - const ExprNode& formula); + ExprNode& formula); bool do_proof_place_ablewaitinf(const SubstList& discrete_state, const DBM& zone, DBMList* place) const; bool do_proof_place_unablewaitinf(const SubstList& discrete_state, @@ -650,7 +674,7 @@ protected: /* IMPLEMENTATION PROOF WITHOUT PLACEHOLDERS */ inline bool prover::do_proof_predicate(const SubstList& discrete_state, const DBM& zone, - const ExprNode& formula) { + ExprNode& formula) { bool retVal = false; /* Look in Known True and Known False Sequent Caches */ @@ -723,7 +747,7 @@ inline bool prover::do_proof_predicate(const SubstList& discrete_state, parentRef = cached_fp_sequent; // parentRef to use for recursive call // Recursively solve the right and side of the equation - const ExprNode* rhs = input_pes.lookup_equation(formula.getPredicate()); + ExprNode* rhs = input_pes.lookup_equation(formula.getPredicate()); retVal = do_proof(discrete_state, zone, *rhs); // Restore caller-saved value of parentRef. @@ -750,7 +774,7 @@ inline bool prover::do_proof_predicate(const SubstList& discrete_state, // [FC14] Proof rule \land inline bool prover::do_proof_and(const SubstList& discrete_state, - const DBM& zone, const ExprNode& formula) { + const DBM& zone, ExprNode& formula) { /* Because zone is only changed after it is copied, it can * be passed to both branches. */ bool retVal = do_proof(discrete_state, zone, *formula.getLeft()); @@ -767,7 +791,7 @@ inline bool prover::do_proof_and(const SubstList& discrete_state, */ // [FC14] Proof rule based on \lor_{s_2} inline bool prover::do_proof_or(const SubstList& discrete_state, - const DBM& zone, const ExprNode& formula) { + const DBM& zone, ExprNode& formula) { bool retVal = false; /* Use two placeholders to provide split here */ @@ -807,7 +831,7 @@ inline bool prover::do_proof_or(const SubstList& discrete_state, // [FC14], rules \lor_{l} and \lor_{r} inline bool prover::do_proof_or_simple(const SubstList& discrete_state, const DBM& zone, - const ExprNode& formula) { + ExprNode& formula) { /* Simplified OR does not need to split on placeholders */ bool retVal = do_proof(discrete_state, zone, *formula.getLeft()); if (!retVal) { @@ -818,7 +842,7 @@ inline bool prover::do_proof_or_simple(const SubstList& discrete_state, // [FC14] Rule \forall_{t1} inline bool prover::do_proof_forall(const SubstList& discrete_state, - const DBM& zone, const ExprNode& formula) { + const DBM& zone, ExprNode& formula) { /* Here the model checker looks at the zone of * all time sucessors and then substitutes in * the substitued constraints and sees if the @@ -840,7 +864,7 @@ inline bool prover::do_proof_forall(const SubstList& discrete_state, // [FC14] Proof rules \forall_{ro1}, \forall_{ro2}, \forall_{ro3} inline bool prover::do_proof_forall_rel(const SubstList& discrete_state, const DBM& zone, - const ExprNode& formula) { + ExprNode& formula) { /* Proof methodology: * first, see if \phi_1 is satisfied during the time advance. @@ -1016,7 +1040,7 @@ inline bool prover::do_proof_forall_rel(const SubstList& discrete_state, // [FC14] Proof rule \exists_{t1} inline bool prover::do_proof_exists(const SubstList& discrete_state, - const DBM& zone, const ExprNode& formula) { + const DBM& zone, ExprNode& formula) { /* Support for exists(), written by Peter Fontana */ // This support gives a placeholder variable // and uses a similar method do_proof_place @@ -1068,7 +1092,7 @@ inline bool prover::do_proof_exists(const SubstList& discrete_state, inline bool prover::do_proof_exists_rel(const SubstList& discrete_state, const DBM& zone, - const ExprNode& formula) { + ExprNode& formula) { bool retVal = false; /* First Try to get a placeholder value that works */ @@ -1251,7 +1275,7 @@ inline bool prover::do_proof_exists_rel(const SubstList& discrete_state, } inline bool prover::do_proof_allact(const SubstList& discrete_state, - const DBM& zone, const ExprNode& formula) { + const DBM& zone, ExprNode& formula) { bool retVal = true; /* Enumerate through all transitions */ cpplog(cpplogging::debug) << "\t Proving ALLACT Transitions:----\n" @@ -1346,7 +1370,7 @@ inline bool prover::do_proof_allact(const SubstList& discrete_state, inline bool prover::do_proof_existact(const SubstList& discrete_state, const DBM& zone, - const ExprNode& formula) { + ExprNode& formula) { bool retVal = false; /* Enumerate through all transitions */ @@ -1454,7 +1478,7 @@ inline bool prover::do_proof_existact(const SubstList& discrete_state, } inline bool prover::do_proof_imply(const SubstList& discrete_state, - const DBM& zone, const ExprNode& formula) { + const DBM& zone, ExprNode& formula) { bool retVal = false; /* Here is the one call to comp_ph(...) outside of comp_ph(...) */ DBM zone_lhs(zone); @@ -1482,7 +1506,7 @@ inline bool prover::do_proof_imply(const SubstList& discrete_state, } inline bool prover::do_proof_constraint(const DBM& zone, - const ExprNode& formula) const { + ExprNode& formula) const { bool retVal = (zone <= *(formula.dbm())); cpplog(cpplogging::debug) << "---(" << (retVal ? "V" : "Inv") @@ -1492,13 +1516,13 @@ inline bool prover::do_proof_constraint(const DBM& zone, } inline bool prover::do_proof_sublist(const SubstList& discrete_state, - const DBM& zone, const ExprNode& formula) { + const DBM& zone, ExprNode& formula) { SubstList st(formula.getSublist(), &discrete_state); return do_proof(st, zone, *formula.getExpr()); } inline bool prover::do_proof_reset(const SubstList& discrete_state, - const DBM& zone, const ExprNode& formula) { + const DBM& zone, ExprNode& formula) { DBM lhs_reset(zone); lhs_reset.reset(*formula.getClockSet()); lhs_reset.cf(); @@ -1506,7 +1530,7 @@ inline bool prover::do_proof_reset(const SubstList& discrete_state, } inline bool prover::do_proof_assign(const SubstList& discrete_state, - const DBM& zone, const ExprNode& formula) { + const DBM& zone, ExprNode& formula) { // Formula is phi[x:=y] with x and y clocks. DBM lhs_assign(zone); lhs_assign.reset(formula.getcX(), formula.getcY()); @@ -1515,7 +1539,7 @@ inline bool prover::do_proof_assign(const SubstList& discrete_state, } inline bool prover::do_proof_replace(const SubstList& discrete_state, - const DBM& zone, const ExprNode& formula) { + const DBM& zone, ExprNode& formula) { SubstList sub_(discrete_state); sub_[formula.getcX()] = discrete_state.at(formula.getcY()); return do_proof(sub_, zone, *formula.getExpr()); @@ -1524,7 +1548,7 @@ inline bool prover::do_proof_replace(const SubstList& discrete_state, /* IMPLEMENTATION PROVER WITH PLACEHOLDERS */ inline void prover::do_proof_place_predicate(const SubstList& discrete_state, const DBM& zone, DBMList* place, - const ExprNode& formula) { + ExprNode& formula) { ExprNode* e = input_pes.lookup_equation(formula.getPredicate()); /* First look in known true and false sequent tables */ @@ -1633,18 +1657,25 @@ inline void prover::do_proof_place_predicate(const SubstList& discrete_state, inline void prover::do_proof_place_and(const SubstList& discrete_state, const DBM& zone, DBMList* place, - const ExprNode& formula) { + ExprNode& formula) { + DBMList currPlace(*place); do_proof_place(discrete_state, zone, place, *formula.getLeft()); place->cf(); if (!place->emptiness()) { + /* for vacuity reasons, send the largest placeholder possible; + * hence only pass the intersected one if there is no vacuity. */ + if(!options.allVacuity) { + place->intersect(currPlace); + } do_proof_place(discrete_state, zone, place, *formula.getRight()); } + // delete currPlace; } // [FC14] Proof rule \lor_{s2} inline void prover::do_proof_place_or(const SubstList& discrete_state, const DBM& zone, DBMList* place, - const ExprNode& formula) { + ExprNode& formula) { DBMList placeholder_left(*place); do_proof_place(discrete_state, zone, &placeholder_left, *formula.getLeft()); @@ -1666,6 +1697,9 @@ inline void prover::do_proof_place_or(const SubstList& discrete_state, << "Left Placeholder of OR (P): " << placeholder_left << "\nRight Placeholder of OR (P): " << *place << std::endl; } + else if (!options.allVacuity) { + formula.getRight()->setBypassedDuringProof(true); + } place->union_(placeholder_left); place->cf(); @@ -1679,7 +1713,7 @@ inline void prover::do_proof_place_or(const SubstList& discrete_state, inline void prover::do_proof_place_or_simple(const SubstList& discrete_state, const DBM& zone, DBMList* place, - const ExprNode& formula) { + ExprNode& formula) { /* In OR_SIMPLE, the placeholder will either be empty or completely full * in one of the two cases. Hence, fewer comparisons with unions of zones * are needed. */ @@ -1706,6 +1740,9 @@ inline void prover::do_proof_place_or_simple(const SubstList& discrete_state, *place = std::move(placeholder_left); } } + else if (!options.allVacuity) { + formula.getRight()->setBypassedDuringProof(true); + } } @@ -1714,7 +1751,7 @@ inline void prover::do_proof_place_or_simple(const SubstList& discrete_state, inline void prover::do_proof_place_forall(const SubstList& discrete_state, const DBM& zone, DBMList* place, - const ExprNode& formula) { + ExprNode& formula) { /* Here the model checker looks at the zone of * all time sucessors and then substitutes in * the substitued constraints and sees if the @@ -1770,7 +1807,7 @@ inline void prover::do_proof_place_forall(const SubstList& discrete_state, inline void prover::do_proof_place_forall_rel(const SubstList& discrete_state, const DBM& zone, DBMList* place, - const ExprNode& formula) { + ExprNode& formula) { /* Proof methodology: * first, see if \phi_1 is satisfied during the time advance. * If it is, check that phi_2 is true both at and before those @@ -1977,7 +2014,7 @@ inline void prover::do_proof_place_forall_rel(const SubstList& discrete_state, inline void prover::do_proof_place_exists(const SubstList& discrete_state, const DBM& zone, DBMList* place, - const ExprNode& formula) { + ExprNode& formula) { /* First try to get a new placeholder value that works */ DBM lhs_succ(zone); lhs_succ.suc(); @@ -2030,7 +2067,7 @@ inline void prover::do_proof_place_exists(const SubstList& discrete_state, inline void prover::do_proof_place_exists_rel(const SubstList& discrete_state, const DBM& zone, DBMList* place, - const ExprNode& formula) { + ExprNode& formula) { /* First Try to get a placeholder value that works */ DBM zone_succ(zone); zone_succ.suc(); @@ -2188,7 +2225,7 @@ inline void prover::do_proof_place_exists_rel(const SubstList& discrete_state, inline void prover::do_proof_place_allact(const SubstList& discrete_state, const DBM& zone, DBMList* place, - const ExprNode& formula) { + ExprNode& formula) { /* Enumerate through all transitions */ cpplog(cpplogging::debug) << "\t Proving ALLACT Transitions:----\n" << std::endl; @@ -2307,7 +2344,7 @@ inline void prover::do_proof_place_allact(const SubstList& discrete_state, inline void prover::do_proof_place_existact(const SubstList& discrete_state, const DBM& zone, DBMList* place, - const ExprNode& formula) { + ExprNode& formula) { DBMList result(INFTYDBM); // DBM to accumulate the result. result.makeEmpty(); @@ -2409,7 +2446,7 @@ inline void prover::do_proof_place_existact(const SubstList& discrete_state, inline void prover::do_proof_place_imply(const SubstList& discrete_state, const DBM& zone, DBMList* place, - const ExprNode& formula) { + ExprNode& formula) { DBM zone_copy(zone); /* call comp_ph() for efficient proving of IMPLY's left. */ if (comp_ph(zone_copy, *(formula.getLeft()), discrete_state)) { @@ -2434,7 +2471,7 @@ inline void prover::do_proof_place_imply(const SubstList& discrete_state, inline void prover::do_proof_place_constraint(const DBM& zone, DBMList* place, - const ExprNode& formula) const { + ExprNode& formula) const { if (zone <= *(formula.dbm())) { cpplog(cpplogging::debug) << "---(Valid) Leaf DBM (CONSTRAINT) Reached " "with no need for Placeholder----" @@ -2476,7 +2513,7 @@ inline void prover::do_proof_place_constraint(const DBM& zone, } inline bool prover::do_proof_place_bool(DBMList* place, - const ExprNode& formula) const { + ExprNode& formula) const { bool retVal = (formula.getBool()); cpplog(cpplogging::debug) << "---(" << (retVal ? "V" : "Inv") << "alid) Leaf BOOL Reached----" << std::endl @@ -2491,7 +2528,7 @@ inline bool prover::do_proof_place_bool(DBMList* place, inline bool prover::do_proof_place_atomic(const SubstList& discrete_state, DBMList* place, - const ExprNode& formula) const { + ExprNode& formula) const { bool retVal = (discrete_state.at(formula.getAtomic()) == formula.getIntVal()); cpplog(cpplogging::debug) << "---(" << (retVal ? "V" : "Inv") << "alid) Leaf ATOMIC == Reached----" << std::endl @@ -2505,7 +2542,7 @@ inline bool prover::do_proof_place_atomic(const SubstList& discrete_state, inline bool prover::do_proof_place_atomic_not(const SubstList& discrete_state, DBMList* place, - const ExprNode& formula) const { + ExprNode& formula) const { bool retVal = (discrete_state.at(formula.getAtomic()) != formula.getIntVal()); cpplog(cpplogging::debug) << "---(" << (retVal ? "V" : "Inv") << "alid) Leaf ATOMIC != Reached----" << std::endl @@ -2520,7 +2557,7 @@ inline bool prover::do_proof_place_atomic_not(const SubstList& discrete_state, inline bool prover::do_proof_place_atomic_lt(const SubstList& discrete_state, DBMList* place, - const ExprNode& formula) const { + ExprNode& formula) const { bool retVal = (discrete_state.at(formula.getAtomic()) < formula.getIntVal()); cpplog(cpplogging::debug) << "---(" << (retVal ? "V" : "Inv") << "alid) Leaf ATOMIC < Reached----" << std::endl @@ -2535,7 +2572,7 @@ inline bool prover::do_proof_place_atomic_lt(const SubstList& discrete_state, inline bool prover::do_proof_place_atomic_gt(const SubstList& discrete_state, DBMList* place, - const ExprNode& formula) const { + ExprNode& formula) const { bool retVal = (discrete_state.at(formula.getAtomic()) > formula.getIntVal()); cpplog(cpplogging::debug) << "---(" << (retVal ? "V" : "Inv") << "alid) Leaf ATOMIC > Reached----" << std::endl @@ -2548,7 +2585,7 @@ inline bool prover::do_proof_place_atomic_gt(const SubstList& discrete_state, inline bool prover::do_proof_place_atomic_le(const SubstList& discrete_state, DBMList* place, - const ExprNode& formula) const { + ExprNode& formula) const { bool retVal = (discrete_state.at(formula.getAtomic()) <= formula.getIntVal()); cpplog(cpplogging::debug) << "---(" << (retVal ? "V" : "Inv") << "alid) Leaf ATOMIC < Reached----" << std::endl @@ -2563,7 +2600,7 @@ inline bool prover::do_proof_place_atomic_le(const SubstList& discrete_state, inline bool prover::do_proof_place_atomic_ge(const SubstList& discrete_state, DBMList* place, - const ExprNode& formula) const { + ExprNode& formula) const { bool retVal = (discrete_state.at(formula.getAtomic()) >= formula.getIntVal()); cpplog(cpplogging::debug) << "---(" << (retVal ? "V" : "Inv") << "alid) Leaf ATOMIC > Reached----" << std::endl @@ -2578,7 +2615,7 @@ inline bool prover::do_proof_place_atomic_ge(const SubstList& discrete_state, inline void prover::do_proof_place_sublist(const SubstList& discrete_state, const DBM& zone, DBMList* place, - const ExprNode& formula) { + ExprNode& formula) { SubstList st(formula.getSublist(), &discrete_state); do_proof_place(st, zone, place, *formula.getExpr()); } @@ -2586,7 +2623,7 @@ inline void prover::do_proof_place_sublist(const SubstList& discrete_state, inline void prover::do_proof_place_reset(const SubstList& discrete_state, const DBM& zone, DBMList* place, - const ExprNode& formula) { + ExprNode& formula) { DBM lhs_reset(zone); // JK: It does not become clear why this is necessary here // lhs_reset.bound(input_pes.max_constant()); @@ -2628,7 +2665,7 @@ inline void prover::do_proof_place_reset(const SubstList& discrete_state, inline void prover::do_proof_place_assign(const SubstList& discrete_state, const DBM& zone, DBMList* place, - const ExprNode& formula) { + ExprNode& formula) { DBM lhs_assign(zone); /* Here the DBM zone is where the value of * clock x is reset to clock y, which is possibly @@ -2671,7 +2708,7 @@ inline void prover::do_proof_place_assign(const SubstList& discrete_state, inline void prover::do_proof_place_replace(const SubstList& discrete_state, const DBM& zone, DBMList* place, - const ExprNode& formula) { + ExprNode& formula) { SubstList sub_(discrete_state); sub_[formula.getcX()] = discrete_state.at(formula.getcY()); do_proof_place(sub_, zone, place, *formula.getExpr()); diff --git a/pes.timed/prover_options.hh b/pes.timed/prover_options.hh index f72ef68..80d3d1a 100644 --- a/pes.timed/prover_options.hh +++ b/pes.timed/prover_options.hh @@ -24,13 +24,9 @@ struct prover_options { * print regular output. */ bool tabled; - /* If True, enable simple vacuity. Else, run - * without simple vacuity. */ - bool simple_vacuity; - /* If True, enable full vacuity. Else, run - * without full vacuity. */ - bool full_vacuity; + * with simple vacuity. */ + bool allVacuity; /** The size of the Hash table of Sequents: nBits + 1 */ unsigned long nHash; diff --git a/pes.timed/test/dbmlisttest.cc b/pes.timed/test/dbmlisttest.cc deleted file mode 100644 index d0ec37f..0000000 --- a/pes.timed/test/dbmlisttest.cc +++ /dev/null @@ -1,441 +0,0 @@ -/** - * Unit tests for DBMList. - * - * - * @author Peter Fontana - * @author Jeroen Keiren - * @copyright MIT Licence, see the accompanying LICENCE.txt. - */ - -#include -#include "DBMList.hh" -#include "testdbms.hh" -#include "gtest/gtest.h" - -/** Use this function only for testing! */ -bool strictly_equal(const DBMList& xs, const DBMList& ys) { - return std::equal(xs.begin(), xs.end(), ys.begin(), [](const DBM& x, const DBM& y) { return x == y; }); -} - -// l1b -DBM testDBM3() -{ - DBM testDBM3(0, 1, bound_to_constraint(-1, weak), make_c2()); - return testDBM3; -} - -// l3a -DBM testDBM4() -{ - DBM testDBM4(make_c2()); - testDBM4.addConstraint(1,0, bound_to_constraint(3, weak)); - testDBM4.addConstraint(2,0, bound_to_constraint(3, weak)); - return testDBM4; -} - -// l3b -DBM testDBM5() -{ - DBM testDBM5(make_c2()); - testDBM5.addConstraint(1,0, bound_to_constraint(4, strict)); - testDBM5.addConstraint(2,0, bound_to_constraint(4, strict)); - testDBM5.addConstraint(0,1, bound_to_constraint(-2, weak)); - testDBM5.addConstraint(0,2, bound_to_constraint(-2, weak)); - return testDBM5; -} - -// l3c -DBM testDBM6() -{ - DBM testDBM6(make_c2()); - testDBM6.addConstraint(2, 1, zero_less); - return testDBM6; -} - -// l4a -DBM testDBM7() -{ - DBM testDBM7(make_c2()); - testDBM7.addConstraint(1,0, bound_to_constraint(1, strict)); - testDBM7.addConstraint(0,1, bound_to_constraint(-2, weak)); - return testDBM7; -} - -// d2a -DBM testDBM8() -{ - DBM testDBM8(make_c2()); - testDBM8.addConstraint(0,1, bound_to_constraint(-1, weak)); - testDBM8.cf(); - return testDBM8; -} - -// d2b -DBM testDBM9() -{ - DBM testDBM9(make_c2()); - testDBM9.addConstraint(1,0, bound_to_constraint(1, strict)); - testDBM9.cf(); - return testDBM9; -} - -// tDBM1 -DBMList testDBMList1() -{ - DBM test1(testDBM1()); - DBMList testDBMList1(test1); - return testDBMList1; -} - -// list1 -DBMList testDBMList3() -{ - DBMList testDBMList3(make_c2()); - DBM test3(testDBM3()); - testDBMList3.addDBM(test3); - return testDBMList3; -} - -// list1b -DBMList testDBMList4() -{ - DBM test3(testDBM3()); - DBMList testDBMList4(test3); - return testDBMList4; -} - -// list3 -DBMList testDBMList5() -{ - DBM test4(testDBM4()); - DBM test5(testDBM5()); - DBM test6(testDBM6()); - DBMList testDBMList5(test4); - testDBMList5.addDBM(test5); - testDBMList5.addDBM(test6); - return testDBMList5; -} - -// list4 -DBMList testDBMList6() -{ - DBM test7(testDBM7()); - DBMList testDBMList6(test7); - return testDBMList6; -} - -// dList2 -DBMList testDBMList7() -{ - DBM test8(testDBM8()); - DBM test9(testDBM9()); - DBMList testDBMList7(test8); - testDBMList7.addDBM(test9); - return testDBMList7; -} - -TEST(DBMListTest, Empty) -{ - DBMList list1cf(testDBMList1()); - DBMList list3cf(testDBMList3()); - DBMList list4cf(testDBMList4()); - DBMList list5cf(testDBMList5()); - list1cf.cf(); - list3cf.cf(); - list4cf.cf(); - list5cf.cf(); - - EXPECT_FALSE(list1cf.emptiness()); - EXPECT_FALSE(list3cf.emptiness()); - EXPECT_FALSE(list4cf.emptiness()); - EXPECT_FALSE(list5cf.emptiness()); -} - -TEST(DBMListTest, CanonicalDBMList1) -{ - DBMList canonical = testDBMList1(); - canonical.cf(); - - DBM test1cf(testDBM1cf()); - DBMList expected(test1cf); - EXPECT_EQ(expected, canonical); -} - -TEST(DBMListTest, CanonicalDBMList3) -{ - DBMList canonical = testDBMList3(); - canonical.cf(); - - DBMList expected(make_c2()); - EXPECT_EQ(expected, canonical); -} - -TEST(DBMListTest, CanonicalDBMList4) -{ - DBMList canonical = testDBMList4(); - canonical.cf(); - - DBMList expected = testDBMList4(); - EXPECT_EQ(expected, canonical); -} - -TEST(DBMListTest, CanonicalDBMList5) -{ - DBMList canonical = testDBMList5(); - canonical.cf(); - - DBM testDBM4cf(make_c2()); - testDBM4cf.addConstraint(0,0, zero_le); - testDBM4cf.addConstraint(0,1, zero_le); - testDBM4cf.addConstraint(0,2, zero_le); - testDBM4cf.addConstraint(1,0, bound_to_constraint(3, weak)); - testDBM4cf.addConstraint(1,1, zero_le); - testDBM4cf.addConstraint(1,2, bound_to_constraint(3, weak)); - testDBM4cf.addConstraint(2,0, bound_to_constraint(3, weak)); - testDBM4cf.addConstraint(2,1, bound_to_constraint(3, weak)); - testDBM4cf.addConstraint(2,2, zero_le); - DBM testDBM5cf(make_c2()); - testDBM5cf.addConstraint(0,0, zero_le); - testDBM5cf.addConstraint(0,1, bound_to_constraint(-2, weak)); - testDBM5cf.addConstraint(0,2, bound_to_constraint(-2, weak)); - testDBM5cf.addConstraint(1,0, bound_to_constraint(4, weak)); - testDBM5cf.addConstraint(1,1, zero_le); - testDBM5cf.addConstraint(1,2, bound_to_constraint(2, weak)); - testDBM5cf.addConstraint(2,0, bound_to_constraint(4, strict)); - testDBM5cf.addConstraint(2,1, bound_to_constraint(2, strict)); - testDBM5cf.addConstraint(2,2, zero_le); - DBM testDBM6cf(make_c2()); - testDBM6cf.addConstraint(0,0, zero_le); - testDBM6cf.addConstraint(0,1, zero_less); - testDBM6cf.addConstraint(0,2, zero_le); - testDBM6cf.addConstraint(1,0, infinity); - testDBM6cf.addConstraint(1,1, zero_le); - testDBM6cf.addConstraint(1,2, infinity); - testDBM6cf.addConstraint(2,0, infinity); - testDBM6cf.addConstraint(2,1, zero_less); - testDBM6cf.addConstraint(2,2, zero_le); - - DBMList expected(testDBM4cf); - expected.addDBM(testDBM5cf); - expected.addDBM(testDBM6cf); - expected.cf(); - - EXPECT_EQ(expected, canonical); -} - -TEST(DBMListTest, CanonicalDBMList6) -{ - DBMList canonical = testDBMList6(); - canonical.cf(); - EXPECT_TRUE(canonical.emptiness()); - - DBM empty(emptyDBM3()); - DBMList expected(empty); - EXPECT_EQ(expected, canonical); - -} - -TEST(DBMListTest, CanonicalDBMList7) -{ - DBMList canonical = testDBMList7(); - canonical.cf(); - - DBMList expected = testDBMList7(); - EXPECT_TRUE(strictly_equal(expected, canonical)); -} - -TEST(DBMListTest, PreDBMList1) -{ - DBMList pre = testDBMList1(); - pre.pre(); - - DBM test1pre(testDBM1pre()); - DBMList expected(test1pre); - EXPECT_EQ(expected, pre); -} - -TEST(DBMListTest, PreCfDBMList1) -{ - DBMList precf = testDBMList1(); - precf.pre(); - precf.cf(); - - DBM test1precf(testDBM1precf()); - DBMList expected(test1precf); - EXPECT_EQ(expected, precf); -} - -TEST(DBMListTest, Subset) -{ - DBMList list3 = testDBMList3(); - DBMList list4 = testDBMList4(); - list3.cf(); - list4.cf(); - DBM infty(make_c2()); - infty.cf(); - - EXPECT_TRUE(list3 <= infty); - EXPECT_TRUE(list4 <= infty); - EXPECT_TRUE(list4 <= list3); - EXPECT_FALSE(list3 <= list4); -} - - -TEST(DBMListTest, Superset) -{ - DBMList list3 = testDBMList3(); - DBMList list4 = testDBMList4(); - list3.cf(); - list4.cf(); - DBM infty(make_c2()); - infty.cf(); - - EXPECT_TRUE(list3 >= infty); - EXPECT_FALSE(list4 >= infty); - EXPECT_FALSE(list4 >= list3); - EXPECT_TRUE(list3 >= list4); -} - -TEST(DBMListTest, Equal) -{ - DBMList list3 = testDBMList3(); - DBMList list4 = testDBMList4(); - DBMList empty = testDBMList3(); - empty.makeEmpty(); - DBM infty(make_c2()); - list3.cf(); - list4.cf(); - - EXPECT_TRUE(list3 == infty); - EXPECT_FALSE(list4 == infty); - EXPECT_FALSE(list4 == list3); - EXPECT_FALSE(list3 == list4); - EXPECT_TRUE(empty == DBMList(emptyDBM3())); - EXPECT_EQ(DBMList(emptyDBM3()), empty); -} - -TEST(DBMListTest, DBMList7Test) -{ - DBMList list7orig = testDBMList7(); - DBMList list7 = testDBMList7(); - DBMList* list7copy = new DBMList(list7); - list7.cf(); - list7copy->cf(); - - EXPECT_EQ(list7, *list7copy); - - list7.cf(); - list7copy->cf(); - EXPECT_FALSE(list7.emptiness()); - EXPECT_FALSE(list7copy->emptiness()); - EXPECT_EQ(list7, (*list7copy)); - EXPECT_TRUE(strictly_equal(list7orig, list7)); - EXPECT_TRUE(strictly_equal(list7orig, *list7copy)); - - DBM infty(make_c2()); - infty.cf(); - EXPECT_TRUE(list7 == infty); - EXPECT_TRUE(strictly_equal(list7, list7orig)); - EXPECT_TRUE(list7 >= infty); - EXPECT_TRUE(strictly_equal(list7, list7orig)); - EXPECT_TRUE(list7 <= infty); - EXPECT_TRUE(strictly_equal(list7, list7orig)); - - delete list7copy; -} - -TEST(DBMListTest, CompareDBMList7Self) -{ - DBMList list7 = testDBMList7(); - list7.cf(); - EXPECT_TRUE(list7 <= list7); - EXPECT_TRUE(list7 >= list7); - EXPECT_TRUE(list7 == list7); -} - -TEST(DBMListTest, CompareDBMList7DBM8) -{ - DBMList list7 = testDBMList7(); - DBM dbm8(testDBM8()); - list7.cf(); - - EXPECT_TRUE(list7 >= dbm8); - EXPECT_FALSE(list7 <= dbm8); - EXPECT_FALSE(list7 == dbm8); -} - -TEST(DBMListTest, Intersection) -{ - DBMList list7orig = testDBMList7(); - DBMList list7 = testDBMList7(); - - list7.intersect(list7orig); - list7.cf(); - DBMList expected = list7orig; - DBM test8(testDBM8()); - DBM test9(testDBM9()); - expected.addDBM(test8); - expected.addDBM(test9); - expected.cf(); - - EXPECT_TRUE(strictly_equal(expected, list7)); - - list7.cf(); - EXPECT_TRUE(strictly_equal(list7orig, list7)); -} - -TEST(DBMListTest, CopyAndIntersectSelf) -{ - DBMList list5 = testDBMList5(); - DBMList list6 = testDBMList6(); - DBMList* list5copy = new DBMList(make_c2()); - *list5copy = list5; - - EXPECT_TRUE(strictly_equal(list5, *list5copy)); - list5.cf(); - list5copy->cf(); - - EXPECT_TRUE(list5 <= *list5copy); - EXPECT_TRUE(list5 >= *list5copy); - EXPECT_TRUE(list5 == *list5copy); - - list5.intersect(*list5copy); - DBMList expected = testDBMList5(); - DBM test4(testDBM4()); - DBM test5(testDBM5()); - DBM test6(testDBM6()); - expected.addDBM(test4); - expected.addDBM(test5); - expected.addDBM(test6); - - list5.cf(); - EXPECT_EQ(*list5copy, list5); - - EXPECT_FALSE(strictly_equal(list5, *list5copy)); - EXPECT_FALSE(strictly_equal(list6, *list5copy)); - - list6.cf(); - EXPECT_TRUE(list5 <= *list5copy); - EXPECT_TRUE(list5 >= *list5copy); - EXPECT_TRUE(list5 == *list5copy); - EXPECT_TRUE(list6 <= *list5copy); - EXPECT_FALSE(list6 >= *list5copy); - EXPECT_FALSE(list6 == *list5copy); - - // test copy - list6 = *list5copy; - EXPECT_TRUE(list6 <= *list5copy); - EXPECT_TRUE(list6 >= *list5copy); - EXPECT_TRUE(list6 == *list5copy); - - list6.cf(); - EXPECT_EQ(list5, list6); - - list6.makeEmpty(); - DBM empty(emptyDBM3()); - DBMList emptylist(empty); - EXPECT_EQ(emptylist, list6); - - delete list5copy; - EXPECT_EQ(emptylist, list6); -} diff --git a/pes.timed/test/dbmtest.cc b/pes.timed/test/dbmtest.cc deleted file mode 100644 index aca13b1..0000000 --- a/pes.timed/test/dbmtest.cc +++ /dev/null @@ -1,1078 +0,0 @@ -/** - * Unit tests for DBM. - * - * - * @author Peter Fontana - * @author Jeroen Keiren - * @copyright MIT Licence, see the accompanying LICENCE.txt. - */ - -#include -#include "DBM.hh" -#include "testdbms.hh" -#include "gtest/gtest.h" - -TEST(DBMTest, ClockZero) -{ - clock_value_t zero_strict = zero_less; - EXPECT_EQ(0x0000, zero_strict); - clock_value_t zero_nonstrict = zero_le; - EXPECT_EQ(0x0001, zero_nonstrict); - EXPECT_EQ(zero_strict, bound_to_constraint(0, strict)); - EXPECT_EQ(zero_nonstrict, bound_to_constraint(0, weak)); -} - -TEST(DBMTest, ClockInfty) -{ - clock_value_t infty_strict = infinity; - EXPECT_EQ(infty_strict, std::numeric_limits::max() ^ 1); -} - -TEST(DBMTest, ClockPositive) -{ - clock_value_t one_strict = bound_to_constraint(1, strict); - EXPECT_EQ(0x0002, one_strict); - clock_value_t one_nonstrict = bound_to_constraint(1, weak); - EXPECT_EQ(0x0003, one_nonstrict); - - clock_value_t three_strict = bound_to_constraint(3, strict); - EXPECT_EQ(0x0006, three_strict); - clock_value_t three_nonstrict = bound_to_constraint(3, weak); - EXPECT_EQ(0x0007, three_nonstrict); -} - -TEST(DBMTest, ClockNegative) -{ - clock_value_t neg_one_strict = bound_to_constraint(-1, strict); - EXPECT_EQ(static_cast(0xFFFE), neg_one_strict); // 2's complement repr. of -2 - clock_value_t neg_one_nonstrict = bound_to_constraint(-1, weak); - EXPECT_EQ(static_cast(0xFFFF), neg_one_nonstrict); // 2's complement repr. of -1 - - clock_value_t neg_three_strict = bound_to_constraint(-3, strict); - EXPECT_EQ(static_cast(0xFFFA), neg_three_strict); // 2's complement repr. of -6 - clock_value_t neg_three_nonstrict = bound_to_constraint(-3, weak); - EXPECT_EQ(static_cast(0xFFFB), neg_three_nonstrict); // 2's complement repr. of -5 -} - -DBM testDBM2() -{ - DBM testDBM2(testDBM1()); - testDBM2.addConstraint(2,1, bound_to_constraint(1, weak)); - return testDBM2; -} - -DBM testDBM3() -{ - // Make a third test DBM - DBM testDBM3(make_c2()); - testDBM3.addConstraint(0,0, bound_to_constraint(0, weak)); - testDBM3.addConstraint(0,1, bound_to_constraint(-3, weak)); - testDBM3.addConstraint(0,2, infinity); - testDBM3.addConstraint(1,0, infinity); - testDBM3.addConstraint(1,1, zero_le); - testDBM3.addConstraint(1,2, bound_to_constraint(-5, weak)); - testDBM3.addConstraint(2,0, infinity); - testDBM3.addConstraint(2,1, bound_to_constraint(7, weak)); - testDBM3.addConstraint(2,2, zero_le); - return testDBM3; -} - -DBM testDBM4() -{ - // Make a fourth test DBM - empty - // This is only empty because the (0, <=) becomes (0,<) - // and illustrates a bug in cf() - DBM testDBM4(make_c2()); - testDBM4.addConstraint(0,0, zero_le); - testDBM4.addConstraint(0,1, bound_to_constraint(-3, weak)); - testDBM4.addConstraint(0,2, infinity); - testDBM4.addConstraint(1,0, bound_to_constraint(3, strict)); - testDBM4.addConstraint(1,1, zero_le); - testDBM4.addConstraint(1,2, infinity); - testDBM4.addConstraint(2,0, infinity); - testDBM4.addConstraint(2,1, infinity); - testDBM4.addConstraint(2,2, zero_le); - return testDBM4; -} - -DBM testDBM5() -{ - // Make a fifth test DBM - empty - DBM testDBM5(make_c2()); - testDBM5.addConstraint(0,0, zero_le); - testDBM5.addConstraint(0,1, bound_to_constraint(-4, weak)); - testDBM5.addConstraint(0,2, infinity); - testDBM5.addConstraint(1,0, bound_to_constraint(2, strict)); - testDBM5.addConstraint(1,1, zero_le); - testDBM5.addConstraint(1,2, infinity); - testDBM5.addConstraint(2,0, infinity); - testDBM5.addConstraint(2,1, infinity); - testDBM5.addConstraint(2,2, zero_le); - return testDBM5; -} - -DBM testDBM6() -{ - // Make a sixth test DBM - empty - DBM testDBM6(make_c2()); - testDBM6.addConstraint(0,0, zero_le); - testDBM6.addConstraint(0,1, bound_to_constraint(-1, weak)); - testDBM6.addConstraint(0,2, bound_to_constraint(-1, weak)); - testDBM6.addConstraint(1,0, bound_to_constraint(1, weak)); - testDBM6.addConstraint(1,1, zero_le); - testDBM6.addConstraint(1,2, zero_le); - testDBM6.addConstraint(2,0, bound_to_constraint(2, strict)); - testDBM6.addConstraint(2,1, bound_to_constraint(1, weak)); - testDBM6.addConstraint(2,2, zero_le); - return testDBM6; -} - -DBM testDBM7() -{ - // Make a seventh test DBM - empty - DBM testDBM7(make_c2()); - testDBM7.addConstraint(0,0, zero_le); - testDBM7.addConstraint(0,1, bound_to_constraint(-3, weak)); - testDBM7.addConstraint(0,2, bound_to_constraint(-1, weak)); - testDBM7.addConstraint(1,0, bound_to_constraint(3, weak)); - testDBM7.addConstraint(1,1, zero_le); - testDBM7.addConstraint(1,2, bound_to_constraint(3, weak)); - testDBM7.addConstraint(2,0, bound_to_constraint(6, strict)); - testDBM7.addConstraint(2,1, bound_to_constraint(3, weak)); - testDBM7.addConstraint(2,2, zero_le); - return testDBM7; -} - -DBM testDBM8() -{ - DBM testDBM8(make_c3()); - testDBM8.addConstraint(0,1, bound_to_constraint(-1, weak)); - testDBM8.addConstraint(3,1, bound_to_constraint(6, weak)); - testDBM8.addConstraint(3,2, bound_to_constraint(4, weak)); - return testDBM8; -} - -DBM testDBM9() -{ - DBM testDBM9(make_c3()); - testDBM9.addConstraint(0,1, bound_to_constraint(-1, weak)); - testDBM9.addConstraint(3,2, bound_to_constraint(4, weak)); - return testDBM9; -} - -DBM testDBM10() -{ - DBM testDBM10(make_c3()); - testDBM10.addConstraint(3,1, bound_to_constraint(6, weak)); - testDBM10.addConstraint(3,2, bound_to_constraint(4, weak)); - return testDBM10; -} - -DBM testDBM11() -{ - DBM testDBM11(make_c3()); - testDBM11.addConstraint(2,0,bound_to_constraint(3, weak)); - return testDBM11; -} - -TEST(DBMTest, DefaultIsInfty) -{ - DBM INFTYDBM(make_c2()); - for(size_t i = 0; i <= make_c2()->size();i++) { - for(size_t j = 0; j < make_c2()->size(); j++){ - if(i == j || i == 0){ - INFTYDBM.addConstraint(i,j, zero_le); - } - else { - INFTYDBM.addConstraint(i,j, infinity); - } - } - } - DBM defaultDBM(make_c2()); - EXPECT_EQ(INFTYDBM, defaultDBM); -} - -TEST(DBMTest, Copy) -{ - DBM copy = testDBM1(); - EXPECT_EQ(testDBM1(), copy); -} - -TEST(DBMTest, Emptiness) -{ - EXPECT_TRUE(emptyDBM3().emptiness()); - EXPECT_FALSE(testDBM1().cf().emptiness()); - EXPECT_TRUE(testDBM2().cf().emptiness()); - EXPECT_FALSE(testDBM3().cf().emptiness()); - EXPECT_TRUE(testDBM4().cf().emptiness()); - EXPECT_TRUE(testDBM5().cf().emptiness()); - EXPECT_FALSE(testDBM6().cf().emptiness()); - EXPECT_FALSE(testDBM7().cf().emptiness()); - EXPECT_FALSE(DBM(make_c2()).cf().emptiness()); -} - -TEST(DBMTest, PreEmptyIsEmpty) -{ - DBM preEmpty(emptyDBM3()); - preEmpty.pre(); - preEmpty.cf(); - EXPECT_TRUE(preEmpty.emptiness()); -} - -TEST(DBMTest, CanonicalEmpty) -{ - EXPECT_TRUE(emptyDBM3().cf().emptiness()); - EXPECT_EQ(emptyDBM3(), emptyDBM3().cf()); -} - -TEST(DBMTest, CanonicalDBM1) -{ - DBM canonical(testDBM1()); - canonical.cf(); - EXPECT_FALSE(canonical.emptiness()); - EXPECT_EQ(testDBM1cf(), canonical); -} - -TEST(DBMTest, CanonicalDBM2) -{ - DBM canonical(testDBM2()); - canonical.cf(); - EXPECT_TRUE(canonical.emptiness()); - EXPECT_EQ(emptyDBM3(), canonical); -} - -TEST(DBMTest, CanonicalDBM3) -{ - DBM canonical(testDBM3()); - canonical.cf(); - EXPECT_FALSE(canonical.emptiness()); - - // DBM in canonical form (expected result) - DBM expected(make_c2()); - expected.addConstraint(0,0, zero_le); - expected.addConstraint(0,1, bound_to_constraint(-3, weak)); - expected.addConstraint(0,2, bound_to_constraint(-8, weak)); - expected.addConstraint(1,0, infinity); - expected.addConstraint(1,1, zero_le); - expected.addConstraint(1,2, bound_to_constraint(-5, weak)); - expected.addConstraint(2,0, infinity); - expected.addConstraint(2,1, bound_to_constraint(7, weak)); - expected.addConstraint(2,2, zero_le); - - EXPECT_EQ(expected, canonical); -} - -TEST(DBMTest, CanonicalDBM4) -{ - DBM canonical(testDBM4()); - canonical.cf(); - EXPECT_TRUE(canonical.emptiness()); - EXPECT_EQ(emptyDBM3(), canonical); -} - -TEST(DBMTest, CanonicalDBM5) -{ - DBM canonical(testDBM5()); - canonical.cf(); - EXPECT_TRUE(canonical.emptiness()); - EXPECT_EQ(emptyDBM3(), canonical); -} - -TEST(DBMTest, CanonicalDBM6) -{ - DBM canonical(testDBM6()); - canonical.cf(); - EXPECT_FALSE(canonical.emptiness()); - - // DBM in canonical form (expected result) - DBM expected(make_c2()); - expected.addConstraint(0,0, zero_le); - expected.addConstraint(0,1, bound_to_constraint(-1, weak)); - expected.addConstraint(0,2, bound_to_constraint(-1, weak)); - expected.addConstraint(1,0, bound_to_constraint(1, weak)); - expected.addConstraint(1,1, zero_le); - expected.addConstraint(1,2, zero_le); - expected.addConstraint(2,0, bound_to_constraint(2, strict)); - expected.addConstraint(2,1, bound_to_constraint(1, strict)); - expected.addConstraint(2,2, zero_le); - - EXPECT_EQ(expected, canonical); -} - -TEST(DBMTest, CanonicalDBM7) -{ - DBM canonical(testDBM7()); - canonical.cf(); - EXPECT_FALSE(canonical.emptiness()); - - // DBM in canonical form (expected result) - DBM expected(make_c2()); - expected.addConstraint(0,0, zero_le); - expected.addConstraint(0,1, bound_to_constraint(-3, weak)); - expected.addConstraint(0,2, bound_to_constraint(-1, weak)); - expected.addConstraint(1,0, bound_to_constraint(3, weak)); - expected.addConstraint(1,1, zero_le); - expected.addConstraint(1,2, bound_to_constraint(2, weak)); - expected.addConstraint(2,0, bound_to_constraint(6, strict)); - expected.addConstraint(2,1, bound_to_constraint(3, strict)); - expected.addConstraint(2,2, zero_le); - - EXPECT_EQ(expected, canonical); -} - -TEST(DBMTest, PreDBM1) -{ - DBM pre(testDBM1()); - pre.pre(); - - EXPECT_EQ(testDBM1pre(), pre); -} - -TEST(DBMTest, PreCanonicalDBM1) -{ - DBM pre_cf(testDBM1()); - pre_cf.pre(); - pre_cf.cf(); - - EXPECT_EQ(testDBM1precf(), pre_cf); -} - -TEST(DBMTest, PreCanonicalStrictDBM1) -{ - DBM strict_pred(testDBM1precf()); - strict_pred.predClosureRev(); - - // DBM in canonical form (expected result) - DBM expected(make_c2()); - expected.addConstraint(0,0, zero_le); - expected.addConstraint(0,1, zero_le); - expected.addConstraint(0,2, zero_le); - expected.addConstraint(1,0, bound_to_constraint(3, strict)); - expected.addConstraint(1,1, zero_le); - expected.addConstraint(1,2, bound_to_constraint(3, strict)); - expected.addConstraint(2,0, bound_to_constraint(7, strict)); - expected.addConstraint(2,1, bound_to_constraint(7, strict)); - expected.addConstraint(2,2, zero_le); - - EXPECT_EQ(expected, strict_pred); -} - -TEST(DBMTest, AddDBM1) -{ - DBM add(testDBM1()); - add.addConstraint(0,1, bound_to_constraint(-2, weak)); - - DBM expected(make_c2()); - expected.addConstraint(0,0, zero_le); - expected.addConstraint(0,1, bound_to_constraint(-2, weak)); - expected.addConstraint(0,2, bound_to_constraint(-5, weak)); - expected.addConstraint(1,0, bound_to_constraint(3, weak)); - expected.addConstraint(1,1, zero_le); - expected.addConstraint(1,2, infinity); - expected.addConstraint(2,0, bound_to_constraint(7, weak)); - expected.addConstraint(2,1, infinity); - expected.addConstraint(2,2, zero_le); - - EXPECT_EQ(expected, add); -} - -TEST(DBMTest, AddCanonicalDBM1) -{ - DBM add_canonical(testDBM1()); - add_canonical.addConstraint(0,1, bound_to_constraint(-2, weak)); - add_canonical.cf(); - - DBM expected(make_c2()); - expected.addConstraint(0,0, zero_le); - expected.addConstraint(0,1, bound_to_constraint(-2, weak)); - expected.addConstraint(0,2, bound_to_constraint(-5, weak)); - expected.addConstraint(1,0, bound_to_constraint(3, weak)); - expected.addConstraint(1,1, zero_le); - expected.addConstraint(1,2, bound_to_constraint(-2, weak)); - expected.addConstraint(2,0, bound_to_constraint(7, weak)); - expected.addConstraint(2,1, bound_to_constraint(5, weak)); - expected.addConstraint(2,2, zero_le); - - EXPECT_EQ(expected, add_canonical); -} - -// TODO: The following test is copied from the original, but it should be -// performed on the DBM that has not been changed to canonical form, I think. -TEST(DBMTest, CanonicalBound3DBM2) -{ - DBM bound3(testDBM2()); - bound3.cf(); - bound3.bound(3); - bound3.cf(); - - EXPECT_TRUE(bound3.emptiness()); - EXPECT_EQ(emptyDBM3(), bound3); -} - -TEST(DBMTest, IntersectDBM7DBM6) -{ - DBM left(testDBM7()); - left.cf(); - DBM right(testDBM6()); - right.cf(); - - left.intersect(right); - - DBM expected(make_c2()); - expected.addConstraint(0,0, zero_le); - expected.addConstraint(0,1, bound_to_constraint(-3, weak)); - expected.addConstraint(0,2, bound_to_constraint(-1, weak)); - expected.addConstraint(1,0, bound_to_constraint(1, weak)); - expected.addConstraint(1,1, zero_le); - expected.addConstraint(1,2, zero_le); - expected.addConstraint(2,0, bound_to_constraint(2, strict)); - expected.addConstraint(2,1, bound_to_constraint(1, strict)); - expected.addConstraint(2,2, zero_le); - - EXPECT_EQ(expected, left); - - left.cf(); - EXPECT_TRUE(left.emptiness()); -} - -TEST(DBMTest, IntersectDBM8DBM6) -{ - DBM left(testDBM7()); - left.cf(); - DBM right(testDBM6()); - right.cf(); - - left.intersect(right); - - DBM expected(make_c2()); - expected.addConstraint(0,0, zero_le); - expected.addConstraint(0,1, bound_to_constraint(-3, weak)); - expected.addConstraint(0,2, bound_to_constraint(-1, weak)); - expected.addConstraint(1,0, bound_to_constraint(1, weak)); - expected.addConstraint(1,1, zero_le); - expected.addConstraint(1,2, zero_le); - expected.addConstraint(2,0, bound_to_constraint(2, strict)); - expected.addConstraint(2,1, bound_to_constraint(1, strict)); - expected.addConstraint(2,2, zero_le); - - EXPECT_EQ(expected, left); - left.cf(); - EXPECT_TRUE(left.emptiness()); - EXPECT_EQ(emptyDBM3(), left); -} - -TEST(DBMTest, IntersectDBM8DBM6heap) -{ - DBM* left = new DBM(testDBM7()); - left->cf(); - DBM right(testDBM6()); - right.cf(); - - left->intersect(right); - - DBM expected(make_c2()); - expected.addConstraint(0,0, zero_le); - expected.addConstraint(0,1, bound_to_constraint(-3, weak)); - expected.addConstraint(0,2, bound_to_constraint(-1, weak)); - expected.addConstraint(1,0, bound_to_constraint(1, weak)); - expected.addConstraint(1,1, zero_le); - expected.addConstraint(1,2, zero_le); - expected.addConstraint(2,0, bound_to_constraint(2, strict)); - expected.addConstraint(2,1, bound_to_constraint(1, strict)); - expected.addConstraint(2,2, zero_le); - - EXPECT_EQ(expected, *left); - left->cf(); - EXPECT_TRUE(left->emptiness()); - EXPECT_EQ(emptyDBM3(), *left); -} - -TEST(DBMTest, IntersectDBM8DBM6reference) -{ - DBM temp(testDBM7()); - DBM* left = &temp; - - left->cf(); - DBM right(testDBM6()); - right.cf(); - - left->intersect(right); - - DBM expected(make_c2()); - expected.addConstraint(0,0, zero_le); - expected.addConstraint(0,1, bound_to_constraint(-3, weak)); - expected.addConstraint(0,2, bound_to_constraint(-1, weak)); - expected.addConstraint(1,0, bound_to_constraint(1, weak)); - expected.addConstraint(1,1, zero_le); - expected.addConstraint(1,2, zero_le); - expected.addConstraint(2,0, bound_to_constraint(2, strict)); - expected.addConstraint(2,1, bound_to_constraint(1, strict)); - expected.addConstraint(2,2, zero_le); - - EXPECT_EQ(expected, *left); - left->cf(); - EXPECT_TRUE(left->emptiness()); - EXPECT_EQ(emptyDBM3(), *left); -} - -TEST(DBMTest, ccrepA) -{ - DBM ccrepA(make_c4()); - for (int i=0; i<5; i++) { - ccrepA.addConstraint(i,0, zero_le); - } - - ccrepA.cf(); - EXPECT_FALSE(ccrepA.emptiness()); - - DBM expected(make_c4()); - for (int i=0; i < 5; i++) { - for (int j=0; j < 5; j++) { - expected.addConstraint(i,j, zero_le); - } - } - EXPECT_EQ(expected, ccrepA); - -} - -TEST(DBMTest, empty) -{ - DBM expected(make_c2()); - for (int i=0; i < 3; i++) { - for (int j=0; j < 3; j++) { - expected.addConstraint(i,j, (0x0)); - } - } - EXPECT_EQ(expected, emptyDBM3()); -} - -// Extra tests -TEST(DBMTest, tDBM5) -{ - DBM test(make_c2()); - test.addConstraint(0,2, bound_to_constraint(-3, weak)); - test.addConstraint(1,0, bound_to_constraint(2, weak)); - test.addConstraint(2,0, bound_to_constraint(2, weak)); - - test.cf(); - EXPECT_TRUE(test.emptiness()); - EXPECT_EQ(emptyDBM3(), test); -} - -TEST(DBMTest, Bound1) -{ - /* Make DBM to try to test the correctnes of bound(maxc) */ - DBM test(make_c2()); - test.addConstraint(0,0, zero_le); - test.addConstraint(0,1, bound_to_constraint(-3, weak)); - test.addConstraint(0,2, infinity); - test.addConstraint(1,0, infinity); - test.addConstraint(1,1, zero_le); - test.addConstraint(1,2, infinity); - test.addConstraint(2,0, infinity); - test.addConstraint(2,1, infinity); - test.addConstraint(2,2, zero_le); - - DBM canonical(test); - canonical.cf(); - EXPECT_EQ(test, canonical); - EXPECT_FALSE(canonical.emptiness()); - - test.bound(2); - test.cf(); - EXPECT_FALSE(test.emptiness()); - - DBM expected(make_c2()); - expected.addConstraint(0,0, zero_le); - expected.addConstraint(0,1, bound_to_constraint(-2, strict)); - expected.addConstraint(0,2, infinity); - expected.addConstraint(1,0, infinity); - expected.addConstraint(1,1, zero_le); - expected.addConstraint(1,2, infinity); - expected.addConstraint(2,0, infinity); - expected.addConstraint(2,1, infinity); - expected.addConstraint(2,2, zero_le); - - EXPECT_EQ(expected, test); -} - -TEST(DBMTest, Bound2) -{ - /* Make DBM to try to test the correctnes of bound(maxc) */ - DBM test(make_c2()); - test.addConstraint(0,0, zero_le); - test.addConstraint(0,1, bound_to_constraint(-5, weak)); - test.addConstraint(0,2, infinity); - test.addConstraint(1,0, infinity); - test.addConstraint(1,1, zero_le); - test.addConstraint(1,2, infinity); - test.addConstraint(2,0, infinity); - test.addConstraint(2,1, bound_to_constraint(2, weak)); - test.addConstraint(2,2, zero_le); - - DBM canonical(test); - canonical.cf(); - EXPECT_EQ(test, canonical); - EXPECT_FALSE(canonical.emptiness()); - - test.bound(4); - test.cf(); - EXPECT_FALSE(test.emptiness()); - - DBM expected(make_c2()); - expected.addConstraint(0,0, zero_le); - expected.addConstraint(0,1, bound_to_constraint(-4, strict)); - expected.addConstraint(0,2, infinity); - expected.addConstraint(1,0, infinity); - expected.addConstraint(1,1, zero_le); - expected.addConstraint(1,2, infinity); - expected.addConstraint(2,0, infinity); - expected.addConstraint(2,1, infinity); - expected.addConstraint(2,2, zero_le); - - EXPECT_EQ(expected, test); -} - -TEST(DBMTest, Bound3) -{ - /* Make DBM to try to test the correctnes of bound(maxc) */ - DBM test(make_c2()); - test.addConstraint(0,0, zero_le); - test.addConstraint(0,1, bound_to_constraint(-5, weak)); - test.addConstraint(0,2, infinity); - test.addConstraint(1,0, infinity); - test.addConstraint(1,1, zero_le); - test.addConstraint(1,2, infinity); - test.addConstraint(2,0, bound_to_constraint(1, weak)); - test.addConstraint(2,1, bound_to_constraint(2, weak)); - test.addConstraint(2,2, zero_le); - - // DBM in canonical form, test canonisation works for this instance. - DBM canonical(make_c2()); - canonical.addConstraint(0,0, zero_le); - canonical.addConstraint(0,1, bound_to_constraint(-5, weak)); - canonical.addConstraint(0,2, infinity); - canonical.addConstraint(1,0, infinity); - canonical.addConstraint(1,1, zero_le); - canonical.addConstraint(1,2, infinity); - canonical.addConstraint(2,0, bound_to_constraint(1, weak)); - canonical.addConstraint(2,1, bound_to_constraint(-4, weak)); - canonical.addConstraint(2,2, zero_le); - - test.cf(); - EXPECT_EQ(canonical, test); - EXPECT_FALSE(test.emptiness()); - - // Finally test bounding. - DBM expected(make_c2()); - expected.addConstraint(0,0, zero_le); - expected.addConstraint(0,1, bound_to_constraint(-4, strict)); - expected.addConstraint(0,2, infinity); - expected.addConstraint(1,0, infinity); - expected.addConstraint(1,1, zero_le); - expected.addConstraint(1,2, infinity); - expected.addConstraint(2,0, bound_to_constraint(1, weak)); - expected.addConstraint(2,1, bound_to_constraint(-3, strict)); - expected.addConstraint(2,2, zero_le); - - test.bound(4); - test.cf(); - EXPECT_FALSE(test.emptiness()); - EXPECT_EQ(expected, test); -} - -TEST(DBMTest, Bound4) -{ - /* Make DBM to try to test the correctnes of bound(maxc) */ - DBM test(make_c2()); - test.addConstraint(0,0, zero_le); - test.addConstraint(0,1, bound_to_constraint(-5, weak)); - test.addConstraint(0,2, infinity); - test.addConstraint(1,0, infinity); - test.addConstraint(1,1, zero_le); - test.addConstraint(1,2, infinity); - test.addConstraint(2,0, zero_le); - test.addConstraint(2,1, bound_to_constraint(2, weak)); - test.addConstraint(2,2, zero_le); - - // DBM in canonical form, test canonisation works for this instance. - DBM canonical(make_c2()); - canonical.addConstraint(0,0, zero_le); - canonical.addConstraint(0,1, bound_to_constraint(-5, weak)); - canonical.addConstraint(0,2, infinity); - canonical.addConstraint(1,0, infinity); - canonical.addConstraint(1,1, zero_le); - canonical.addConstraint(1,2, infinity); - canonical.addConstraint(2,0, zero_le); - canonical.addConstraint(2,1, bound_to_constraint(-5, weak)); - canonical.addConstraint(2,2, zero_le); - - test.cf(); - EXPECT_EQ(canonical, test); - EXPECT_FALSE(test.emptiness()); - - // Finally test bounding. - DBM expected(make_c2()); - expected.addConstraint(0,0, zero_le); - expected.addConstraint(0,1, bound_to_constraint(-4, strict)); - expected.addConstraint(0,2, infinity); - expected.addConstraint(1,0, infinity); - expected.addConstraint(1,1, zero_le); - expected.addConstraint(1,2, infinity); - expected.addConstraint(2,0, zero_le); - expected.addConstraint(2,1, bound_to_constraint(-4, strict)); - expected.addConstraint(2,2, zero_le); - - test.bound(4); - test.cf(); - EXPECT_FALSE(test.emptiness()); - EXPECT_EQ(expected, test); -} - -TEST(DBMTest, Bound5) -{ - /* Make DBM to try to test the correctnes of bound(maxc) */ - DBM test(make_c2()); - test.addConstraint(0,0, zero_le); - test.addConstraint(0,1, bound_to_constraint(-5, weak)); - test.addConstraint(0,2, infinity); - test.addConstraint(1,0, infinity); - test.addConstraint(1,1, zero_le); - test.addConstraint(1,2, infinity); - test.addConstraint(2,0, bound_to_constraint(-1, weak)); - test.addConstraint(2,1, bound_to_constraint(2, weak)); - test.addConstraint(2,2, zero_le); - - // DBM in canonical form, test canonisation works for this instance. - DBM canonical(make_c2()); - canonical.addConstraint(0,0, zero_le); - canonical.addConstraint(0,1, bound_to_constraint(-5, weak)); - canonical.addConstraint(0,2, infinity); - canonical.addConstraint(1,0, infinity); - canonical.addConstraint(1,1, zero_le); - canonical.addConstraint(1,2, infinity); - canonical.addConstraint(2,0, bound_to_constraint(-1, weak)); - canonical.addConstraint(2,1, bound_to_constraint(-6, weak)); - canonical.addConstraint(2,2, zero_le); - - test.cf(); - EXPECT_EQ(canonical, test); - EXPECT_FALSE(test.emptiness()); - - // Finally test bounding. - DBM expected(make_c2()); - expected.addConstraint(0,0, zero_le); - expected.addConstraint(0,1, bound_to_constraint(-4, strict)); - expected.addConstraint(0,2, infinity); - expected.addConstraint(1,0, infinity); - expected.addConstraint(1,1, zero_le); - expected.addConstraint(1,2, infinity); - expected.addConstraint(2,0, bound_to_constraint(-1, weak)); - expected.addConstraint(2,1, bound_to_constraint(-4, strict)); - expected.addConstraint(2,2, zero_le); - - test.bound(4); - EXPECT_EQ(expected, test); - test.cf(); - EXPECT_FALSE(test.emptiness()); -} - -TEST(DBMTest, Bound6) -{ - /* Make DBM to try to test the correctnes of bound(maxc) */ - DBM test(make_c2()); - test.addConstraint(0,0, zero_le); - test.addConstraint(0,1, bound_to_constraint(-2, weak)); - test.addConstraint(0,2, infinity); - test.addConstraint(1,0, infinity); - test.addConstraint(1,1, zero_le); - test.addConstraint(1,2, bound_to_constraint(1, strict)); - test.addConstraint(2,0, infinity); - test.addConstraint(2,1, infinity); - test.addConstraint(2,2, zero_le); - - // DBM in canonical form, test canonisation works for this instance. - DBM canonical(make_c2()); - canonical.addConstraint(0,0, zero_le); - canonical.addConstraint(0,1, bound_to_constraint(-2, weak)); - canonical.addConstraint(0,2, bound_to_constraint(-1, strict)); - canonical.addConstraint(1,0, infinity); - canonical.addConstraint(1,1, zero_le); - canonical.addConstraint(1,2, bound_to_constraint(1, strict)); - canonical.addConstraint(2,0, infinity); - canonical.addConstraint(2,1, infinity); - canonical.addConstraint(2,2, zero_le); - - test.cf(); - EXPECT_EQ(canonical, test); - EXPECT_FALSE(test.emptiness()); - - // Finally test bounding. - DBM expected(make_c2()); - expected.addConstraint(0,0, zero_le); - expected.addConstraint(0,1, bound_to_constraint(-1, strict)); - expected.addConstraint(0,2, bound_to_constraint(-1, strict)); - expected.addConstraint(1,0, infinity); - expected.addConstraint(1,1, zero_le); - expected.addConstraint(1,2, bound_to_constraint(1, strict)); - expected.addConstraint(2,0, infinity); - expected.addConstraint(2,1, infinity); - expected.addConstraint(2,2, zero_le); - - test.bound(1); - test.cf(); - EXPECT_FALSE(test.emptiness()); - EXPECT_EQ(expected, test); -} - -TEST(DBMTest, Empty1) -{ - DBM test(make_c2()); - test.addConstraint(0,0, zero_le); - test.addConstraint(0,1, bound_to_constraint(-5, weak)); - test.addConstraint(0,2, infinity); - test.addConstraint(1,0, infinity); - test.addConstraint(1,1, zero_le); - test.addConstraint(1,2, infinity); - test.addConstraint(2,0, infinity); - test.addConstraint(2,1, bound_to_constraint(2, weak)); - test.addConstraint(2,2, zero_le); - - // DBM is already in cf - DBM canonical(test); - canonical.cf(); - EXPECT_EQ(test, canonical); - EXPECT_FALSE(canonical.emptiness()); - - // Normalize - DBM expected(make_c2()); - expected.addConstraint(0,0, zero_le); - expected.addConstraint(0,1, bound_to_constraint(-4, strict)); - expected.addConstraint(0,2, infinity); - expected.addConstraint(1,0, infinity); - expected.addConstraint(1,1, zero_le); - expected.addConstraint(1,2, infinity); - expected.addConstraint(2,0, infinity); - expected.addConstraint(2,1, infinity); - expected.addConstraint(2,2, zero_le); - - test.bound(4); - test.cf(); - EXPECT_EQ(expected, test); - EXPECT_FALSE(test.emptiness()); - - DBM canonical_bound(test); - canonical_bound.cf(); - EXPECT_EQ(test, canonical_bound); -} - -TEST(DBMTest, Empty2) -{ - DBM test(testDBM8()); - - // DBM is already in cf - DBM canonical(test); - canonical.cf(); - EXPECT_EQ(test, canonical); - EXPECT_FALSE(canonical.emptiness()); -} - -TEST(DBMTest, Empty3) -{ - DBM test(testDBM9()); - - // DBM is already in cf - DBM canonical(test); - canonical.cf(); - EXPECT_EQ(test, canonical); - EXPECT_FALSE(canonical.emptiness()); -} - -TEST(DBMTest, Empty4) -{ - DBM test(testDBM10()); - - // DBM is already in cf - DBM canonical(test); - canonical.cf(); - EXPECT_EQ(test, canonical); - EXPECT_FALSE(canonical.emptiness()); -} - -TEST(DBMTest, Empty5) -{ - DBM test(testDBM11()); - - DBM canonical(make_c3()); - canonical.addConstraint(0,0, zero_le); - canonical.addConstraint(0,1, zero_le); - canonical.addConstraint(0,2, zero_le); - canonical.addConstraint(0,3, zero_le); - canonical.addConstraint(1,0, infinity); - canonical.addConstraint(1,1, zero_le); - canonical.addConstraint(1,2, infinity); - canonical.addConstraint(1,3, infinity); - canonical.addConstraint(2,0, bound_to_constraint(3, weak)); - canonical.addConstraint(2,1, bound_to_constraint(3, weak)); - canonical.addConstraint(2,2, zero_le); - canonical.addConstraint(2,3, bound_to_constraint(3, weak)); - canonical.addConstraint(3,0, infinity); - canonical.addConstraint(3,1, infinity); - canonical.addConstraint(3,2, infinity); - canonical.addConstraint(3,3, zero_le); - - test.cf(); - EXPECT_EQ(canonical, test); - EXPECT_FALSE(test.emptiness()); -} - -TEST(DBMTest, IntersectDBM11DBM8) -{ - DBM left(testDBM11()); - left.cf(); - DBM right(testDBM8()); - left.intersect(right); - - DBM expected(make_c3()); - expected.addConstraint(0,0, zero_le); - expected.addConstraint(0,1, bound_to_constraint(-1, weak)); - expected.addConstraint(0,2, zero_le); - expected.addConstraint(0,3, zero_le); - expected.addConstraint(1,0, infinity); - expected.addConstraint(1,1, zero_le); - expected.addConstraint(1,2, infinity); - expected.addConstraint(1,3, infinity); - expected.addConstraint(2,0, bound_to_constraint(3, weak)); - expected.addConstraint(2,1, bound_to_constraint(3, weak)); - expected.addConstraint(2,2, zero_le); - expected.addConstraint(2,3, bound_to_constraint(3, weak)); - expected.addConstraint(3,0, infinity); - expected.addConstraint(3,1, bound_to_constraint(6, weak)); - expected.addConstraint(3,2, bound_to_constraint(4, weak)); - expected.addConstraint(3,3, zero_le); - - EXPECT_EQ(expected, left); - - DBM canonical(make_c3()); - canonical.addConstraint(0,0, zero_le); - canonical.addConstraint(0,1, bound_to_constraint(-1, weak)); - canonical.addConstraint(0,2, zero_le); - canonical.addConstraint(0,3, zero_le); - canonical.addConstraint(1,0, infinity); - canonical.addConstraint(1,1, zero_le); - canonical.addConstraint(1,2, infinity); - canonical.addConstraint(1,3, infinity); - canonical.addConstraint(2,0, bound_to_constraint(3, weak)); - canonical.addConstraint(2,1, bound_to_constraint(2, weak)); - canonical.addConstraint(2,2, zero_le); - canonical.addConstraint(2,3, bound_to_constraint(3, weak)); - canonical.addConstraint(3,0, bound_to_constraint(7, weak)); - canonical.addConstraint(3,1, bound_to_constraint(6, weak)); - canonical.addConstraint(3,2, bound_to_constraint(4, weak)); - canonical.addConstraint(3,3, zero_le); - - left.cf(); - EXPECT_EQ(canonical, left); -} - -TEST(DBMTest, IntersectDBM11DBM9) -{ - DBM left(testDBM11()); - DBM right(testDBM9()); - left.intersect(right); - - DBM expected(make_c3()); - expected.addConstraint(0,0, zero_le); - expected.addConstraint(0,1, bound_to_constraint(-1, weak)); - expected.addConstraint(0,2, zero_le); - expected.addConstraint(0,3, zero_le); - expected.addConstraint(1,0, infinity); - expected.addConstraint(1,1, zero_le); - expected.addConstraint(1,2, infinity); - expected.addConstraint(1,3, infinity); - expected.addConstraint(2,0, bound_to_constraint(3, weak)); - expected.addConstraint(2,1, infinity); - expected.addConstraint(2,2, zero_le); - expected.addConstraint(2,3, infinity); - expected.addConstraint(3,0, infinity); - expected.addConstraint(3,1, infinity); - expected.addConstraint(3,2, bound_to_constraint(4, weak)); - expected.addConstraint(3,3, zero_le); - EXPECT_EQ(expected, left); - - DBM canonical(make_c3()); - canonical.addConstraint(0,0, zero_le); - canonical.addConstraint(0,1, bound_to_constraint(-1, weak)); - canonical.addConstraint(0,2, zero_le); - canonical.addConstraint(0,3, zero_le); - canonical.addConstraint(1,0, infinity); - canonical.addConstraint(1,1, zero_le); - canonical.addConstraint(1,2, infinity); - canonical.addConstraint(1,3, infinity); - canonical.addConstraint(2,0, bound_to_constraint(3, weak)); - canonical.addConstraint(2,1, bound_to_constraint(2, weak)); - canonical.addConstraint(2,2, zero_le); - canonical.addConstraint(2,3, bound_to_constraint(3, weak)); - canonical.addConstraint(3,0, bound_to_constraint(7, weak)); - canonical.addConstraint(3,1, bound_to_constraint(6, weak)); - canonical.addConstraint(3,2, bound_to_constraint(4, weak)); - canonical.addConstraint(3,3, zero_le); - - left.cf(); - EXPECT_EQ(canonical, left); -} - -TEST(DBMTest, IntersectDBM11DBM10) -{ - DBM left(testDBM11()); - DBM right(testDBM10()); - left.intersect(right); - - DBM expected(make_c3()); - expected.addConstraint(0,0, zero_le); - expected.addConstraint(0,1, zero_le); - expected.addConstraint(0,2, zero_le); - expected.addConstraint(0,3, zero_le); - expected.addConstraint(1,0, infinity); - expected.addConstraint(1,1, zero_le); - expected.addConstraint(1,2, infinity); - expected.addConstraint(1,3, infinity); - expected.addConstraint(2,0, bound_to_constraint(3, weak)); - expected.addConstraint(2,1, infinity); - expected.addConstraint(2,2, zero_le); - expected.addConstraint(2,3, infinity); - expected.addConstraint(3,0, infinity); - expected.addConstraint(3,1, bound_to_constraint(6, weak)); - expected.addConstraint(3,2, bound_to_constraint(4, weak)); - expected.addConstraint(3,3, zero_le); - EXPECT_EQ(expected, left); - - DBM canonical(make_c3()); - canonical.addConstraint(0,0, zero_le); - canonical.addConstraint(0,1, zero_le); - canonical.addConstraint(0,2, zero_le); - canonical.addConstraint(0,3, zero_le); - canonical.addConstraint(1,0, infinity); - canonical.addConstraint(1,1, zero_le); - canonical.addConstraint(1,2, infinity); - canonical.addConstraint(1,3, infinity); - canonical.addConstraint(2,0, bound_to_constraint(3, weak)); - canonical.addConstraint(2,1, bound_to_constraint(3, weak)); - canonical.addConstraint(2,2, zero_le); - canonical.addConstraint(2,3, bound_to_constraint(3, weak)); - canonical.addConstraint(3,0, bound_to_constraint(7, weak)); - canonical.addConstraint(3,1, bound_to_constraint(6, weak)); - canonical.addConstraint(3,2, bound_to_constraint(4, weak)); - canonical.addConstraint(3,3, zero_le); - - left.cf(); - EXPECT_EQ(canonical, left); -} - -// Call RUN_ALL_TESTS() in main(). -// -// We do this by linking in src/gtest_main.cc file, which consists of -// a main() function which calls RUN_ALL_TESTS() for us. -// -// This runs all the tests we've defined, prints the result, and -// returns 0 if successful, or 1 otherwise. diff --git a/pes.timed/test/parsetest.cc b/pes.timed/test/parsetest.cc deleted file mode 100644 index 0c49967..0000000 --- a/pes.timed/test/parsetest.cc +++ /dev/null @@ -1,58 +0,0 @@ -/** - * Unit tests for Parsing. - * - * @author Jeroen Keiren - * @copyright MIT Licence, see the accompanying LICENCE.txt. - */ - -#include -#include -#include "parse.hh" -#include "gtest/gtest.h" - -#define QUOTE(name) #name -#define STR(macro) QUOTE(macro) -#define EXAMPLES_DIR_NAME STR(EXAMPLES_DIR) - -std::string AFSpecA1String( - "CLOCKS :{x1}\n" - "CONTROL :{p1(2)}\n" - "PREDICATE: {X1}\n" - "START: X1\n" - "EQUATIONS: {\n" - "1: mu X1 = p1 == 1\n" - " || ((\\forall time( \n" - "( (p1 == 0) -> (X1[p1=0][x1]))\n" - "&& ( (p1 == 0) -> (X1[p1=1]))\n" - "&& ( (p1 == 1) -> (X1[p1=1])))))\n" - "}\n" - "INVARIANT:\n" - " p1 == 0 -> x1 <= 2\n"); - -TEST(ParseTest, ParseFile) -{ - pes p; - std::string filename(std::string(EXAMPLES_DIR_NAME) + "/CorrectnessTestSuite/Invalid/Liveness/AFSpecA1.in"); - ASSERT_NO_THROW(parse_pes(filename, false, p)); - - EXPECT_EQ(1, p.clocks()->size()); - EXPECT_EQ(1, p.atomic()->size()); - EXPECT_EQ("X1", p.start_predicate()); -} - -TEST(ParseTest, ParseNonexistantFile) -{ - pes p; - std::string filename(std::string(EXAMPLES_DIR_NAME) + "/Nonexistant.in"); - EXPECT_ANY_THROW(parse_pes(filename, false, p)); -} - -TEST(ParseTest, ParseString) -{ - pes p; - ASSERT_NO_THROW(parse_pes_from_string(AFSpecA1String, false, p)); - - EXPECT_EQ(1, p.clocks()->size()); - EXPECT_EQ(1, p.atomic()->size()); - EXPECT_EQ("X1", p.start_predicate()); -} diff --git a/pes.timed/test/prooftest.cc b/pes.timed/test/prooftest.cc deleted file mode 100644 index fa25c3c..0000000 --- a/pes.timed/test/prooftest.cc +++ /dev/null @@ -1,319 +0,0 @@ -/** - * Unit tests for prover. - * - * @author Jeroen Keiren - * @copyright MIT Licence, see the accompanying LICENCE.txt. - */ - -#include -#include -#include "proof.hh" -#include "parse.hh" -#include "gtest/gtest.h" - -static -std::string AllActBug( - "CLOCKS: {x}\n" - "CONTROL: {p=1}\n" - "INITIALLY: x == 0\n" - "PREDICATE: {X}\n" - "START: X\n" - "EQUATIONS: {\n" - "1: mu X = \\AllAct(X) && p==1\n" - "}\n" - "INVARIANT:\n" - " p == 1 -> x == 0\n" - "TRANSITIONS:\n" - " (p==1)->(p=2);\n"); - -TEST(ProofTest, AllActBugTest) -{ - pes p; - ASSERT_NO_THROW(parse_pes_from_string(AllActBug, false, p)); - - prover_options options; - prover pr(p, options); - EXPECT_FALSE(pr.do_proof_init(p)); -} - -TEST(ProofTest, AllActBugTestPlace) -{ - pes p; - ASSERT_NO_THROW(parse_pes_from_string(AllActBug, false, p)); - - prover_options options; - prover pr(p, options); - DBMList placeholder(DBM(p.clocks())); - placeholder.cf(); - EXPECT_FALSE(pr.do_proof_init(p, &placeholder)); -} - -static -std::string ExistsBug( - "#define CA 3\n" - "CLOCKS :{x1}\n" - "CONTROL :{p1(1)}\n" - "PREDICATE: {X}\n" - "START: X\n" - "EQUATIONS: {\n" - "1: nu X = (\\exists time(x1 <= 2 && \\forall time(x1 >= 4)))\n" - " }\n"); - -TEST(ProofTest, ExistsBugTest) -{ - pes p; - ASSERT_NO_THROW(parse_pes_from_string(ExistsBug, false, p)); - - prover_options options; - prover pr(p, options); - - EXPECT_FALSE(pr.do_proof_init(p)); - -} - -// In the following example, the property does not hold. However, the placeholder -// that is computed for which the property does hold should be non-empty. -static -std::string ExistsRel( - "CLOCKS: {x1,x2}\n" - "CONTROL: {p1}\n" - "INITIALLY: x1 <= 2 && x2<=1\n" - "PREDICATE: {X}\n" - "START: X\n" - "EQUATIONS: {\n" - "1: mu X = \\exists time\\rel[x1 <= 3](x2==3)\n" - "}\n" - "TRANSITIONS:\n" - ); - -TEST(ProofTest, ExistsRelTestFalse) -{ - pes p; - ASSERT_NO_THROW(parse_pes_from_string(ExistsRel, false, p)); - - prover_options options; - prover pr(p, options); - - DBMList placeholder(DBM(p.clocks())); - placeholder.cf(); - EXPECT_FALSE(pr.do_proof_init(p, &placeholder)); - placeholder.cf(); - - DBM minimum_region(p.clocks()); - minimum_region.addConstraint(1,0, bound_to_constraint(2, weak)); - minimum_region.addConstraint(2,0, bound_to_constraint(1, weak)); - minimum_region.addConstraint(1,2, bound_to_constraint(0, weak)); - - DBM maximum_region1(p.clocks()); - maximum_region1.addConstraint(2,0, bound_to_constraint(3, weak)); - maximum_region1.addConstraint(1,2, bound_to_constraint(0, weak)); - - DBM maximum_region2(p.clocks()); - maximum_region2.addConstraint(2,0, bound_to_constraint(3, weak)); - maximum_region2.addConstraint(2,1, bound_to_constraint(-2, weak)); - - DBMList minimum_placeholder(minimum_region); - minimum_placeholder.cf(); - EXPECT_TRUE(minimum_placeholder <= placeholder); - - DBMList maximum_placeholder(maximum_region1); - maximum_placeholder.addDBM(maximum_region2); - maximum_placeholder.cf(); - EXPECT_TRUE(placeholder <= maximum_placeholder); - - - if(!(minimum_placeholder <= placeholder) || !(placeholder <= maximum_placeholder)) - { - std::cerr << "Resulting placeholder: " << placeholder << std::endl; - std::cerr << "Minimal placeholder: " << minimum_placeholder << std::endl; - std::cerr << "Maximal placeholder: " << maximum_placeholder << std::endl; - } -} - -// In the following example, the initial region is exactly equal to the -// part of the initial region that must be included in the placeholder. -// Therefore, the property must hold. -static -std::string ExistsRelSmallRegion( - "CLOCKS: {x1,x2}\n" - "CONTROL: {p1}\n" - "INITIALLY: x1 <= 2 && x2<=1 && x2 - x1 >= 0\n" - "PREDICATE: {X}\n" - "START: X\n" - "EQUATIONS: {\n" - "1: mu X = \\exists time\\rel[x1 <= 3](x2==3)\n" - "}\n" - "TRANSITIONS:\n" - ); - -TEST(ProofTest, ExistsRelTestTrue) -{ - pes p; - ASSERT_NO_THROW(parse_pes_from_string(ExistsRelSmallRegion, false, p)); - - prover_options options; - prover pr(p, options); - - DBMList placeholder(DBM(p.clocks())); - placeholder.cf(); - EXPECT_TRUE(pr.do_proof_init(p, &placeholder)); - placeholder.cf(); - - DBM minimum_region(p.clocks()); - minimum_region.addConstraint(1,0, bound_to_constraint(2, weak)); - minimum_region.addConstraint(2,0, bound_to_constraint(1, weak)); - minimum_region.addConstraint(1,2, bound_to_constraint(0, weak)); - - DBM maximum_region(p.clocks()); - maximum_region.addConstraint(2,0, bound_to_constraint(3, weak)); - - DBMList minimum_placeholder(minimum_region); - minimum_placeholder.cf(); - EXPECT_TRUE(minimum_placeholder <= placeholder); - - DBMList maximum_placeholder(maximum_region); - maximum_placeholder.cf(); - EXPECT_TRUE(placeholder <= maximum_placeholder); - - - if(!(minimum_placeholder <= placeholder) || !(placeholder <= maximum_placeholder)) - { - std::cerr << "Resulting placeholder: " << placeholder << std::endl; - std::cerr << "Minimal placeholder: " << minimum_placeholder << std::endl; - std::cerr << "Maximal placeholder: " << maximum_placeholder << std::endl; - } -} - -// In the following example, the property holds. The reason for the property -// to hold is that the placeholder for the relativized exists accounts for -// x1 <= 2 && x2 <= 1 && x1 - x2 <= 0; the placeholder for the second disjunct -// accounts for the region x2 - x1 <= 0. Therefore, the entire initial region -// is covered. -static -std::string ExistsRelTrueDueToOr( - "CLOCKS: {x1,x2}\n" - "CONTROL: {p1}\n" - "INITIALLY: x1 <= 2 && x2<=1\n" - "PREDICATE: {X}\n" - "START: X\n" - "EQUATIONS: {\n" - "1: mu X = (\\exists time\\rel[x1 <= 3](x2==3)) || x2 - x1 <= 0\n" - "}\n" - "TRANSITIONS:\n" - ); - -TEST(ProofTest, ExistsRelTestTrueDueToOr) -{ - pes p; - ASSERT_NO_THROW(parse_pes_from_string(ExistsRelTrueDueToOr, false, p)); - - prover_options options; - prover pr(p, options); - - DBMList placeholder(DBM(p.clocks())); - placeholder.cf(); - EXPECT_TRUE(pr.do_proof_init(p, &placeholder)); - placeholder.cf(); -} - -static -std::string RelSplit3( - "CLOCKS: {x1}\n" - "CONTROL: {p1}\n" - "INITIALLY: x1 == 0\n" - "PREDICATE: {X}\n" - "START: X\n" - "EQUATIONS: {\n" - "1: nu X = \\exists time\\rel[x1 <2](x1>=2) || \\forall time(x1 < 2)\n" - "}\n" - "INVARIANT:\n" - " p1 == 0 -> x1 < 3\n" - "TRANSITIONS:\n"); - -TEST(ProofTest, RelSplit3Test) -{ - pes p; - ASSERT_NO_THROW(parse_pes_from_string(RelSplit3, false, p)); - - prover_options options; - prover pr(p, options); - - DBMList placeholder(DBM(p.clocks())); - placeholder.cf(); - EXPECT_TRUE(pr.do_proof_init(p, &placeholder)); - placeholder.cf(); -} - -static -std::string ExistsRelFalseFirstSubformula( - "CLOCKS: {x1}\n" - "CONTROL: {p1}\n" - "INITIALLY: x1 == 0\n" - "PREDICATE: {X}\n" - "START: X\n" - "EQUATIONS: {\n" - "1: nu X = \\exists time\\rel[x1 >= 3](x1 <= 3)\n" - "}\n" - "TRANSITIONS:\n"); - -TEST(ProofTest, ExistsRelFalseFirstSubformulaTest) -{ - pes p; - ASSERT_NO_THROW(parse_pes_from_string(ExistsRelFalseFirstSubformula, false, p)); - - prover_options options; - prover pr(p, options); - - DBMList placeholder(DBM(p.clocks())); - placeholder.cf(); - EXPECT_TRUE(pr.do_proof_init(p, &placeholder)); - placeholder.cf(); -} - -static -std::string TrueCache( - "CLOCKS: {x}\n" - "CONTROL: {p=1}\n" - "INITIALLY: x == 0\n" - "PREDICATE: {X}\n" - "START: X\n" - "EQUATIONS: {\n" - "1: nu X = \\AllAct(X) && p!=1\n" - "}\n" - "INVARIANT:\n" - " p == 1 -> x == 0\n" - "TRANSITIONS:\n" - " (p==1)->(p=1);\n"); - -TEST(ProofTest, TrueCacheTest) -{ - pes p; - ASSERT_NO_THROW(parse_pes_from_string(TrueCache, false, p)); - prover_options options; - prover pr(p, options); - EXPECT_FALSE(pr.do_proof_init(p)); -} - -static -std::string FalseCache( - "CLOCKS: {x}\n" - "CONTROL: {p=1}\n" - "INITIALLY: x == 0\n" - "PREDICATE: {X}\n" - "START: X\n" - "EQUATIONS: {\n" - "1: mu X = \\AllAct(X) || p==1\n" - "}\n" - "INVARIANT:\n" - " p == 1 -> x == 0\n" - "TRANSITIONS:\n" - " (p==1)->(p=1);\n"); - -TEST(ProofTest, FalseCacheTest) -{ - pes p; - ASSERT_NO_THROW(parse_pes_from_string(FalseCache, false, p)); - prover_options options; - prover pr(p, options); - EXPECT_TRUE(pr.do_proof_init(p)); -} diff --git a/pes.timed/timesolver-ta.cc b/pes.timed/timesolver-ta.cc index 1a0574a..6821761 100644 --- a/pes.timed/timesolver-ta.cc +++ b/pes.timed/timesolver-ta.cc @@ -47,6 +47,7 @@ #endif #define DEBUG_PLACEHOLDER_PROVER false +#define HIDE_VACUITY_OUTPUT false /** Prints out the "help" info for the user or * the information that is displayed when the @@ -62,10 +63,8 @@ void printUsage() { std::cerr << "\t option: --version print the version of the tool" << std::endl; std::cerr << "\t option: --no-caching/-n disables performance-optimizing " "known true and known false caches. Circularity stack caching " << "still used." << std::endl; - std::cerr << "\t option: --checking-vacuity/-C enables simple vacuity checking " - << std::endl; - std::cerr << "\t option: --vacuity-full/-V enables full vacuity checking " - << std::endl; + std::cerr << "\t option: --full-vacuity/-f enables full vacuity checking. " + << " Simple Vacuity is enabled by default" << std::endl; } void printVersion() { @@ -75,7 +74,7 @@ void printVersion() { /** Parsers the command line */ void parse_command_line(int argc, char** argv, prover_options& opt) { /* Sets parameters and looks for inputs from the command line. */ - const char* const short_opts = "dDhntHCV:"; + const char* const short_opts = "dDhntHf:"; const option long_opts[] { {"debug", 0, nullptr, 'd'}, {"full-debug", 0, nullptr, 'D'}, @@ -84,8 +83,7 @@ void parse_command_line(int argc, char** argv, prover_options& opt) { {"tabled-output", 0, nullptr, 't'}, {"hash", 1, nullptr, 'H'}, {"version", 0, nullptr, 'v'}, - {"simple-vacuity", 0, nullptr, 'C'}, - {"full-vacuity", 0, nullptr, 'V'}, + {"allVacuity", 0, nullptr, 'f'}, {nullptr, 0, nullptr, 0} }; @@ -122,11 +120,8 @@ void parse_command_line(int argc, char** argv, prover_options& opt) { case 'n': opt.useCaching = false; break; - case 'C': - opt.simple_vacuity = true; - break; - case 'V': - opt.full_vacuity = true; + case 'f': + opt.allVacuity = true; break; case 'v': printVersion(); @@ -309,7 +304,48 @@ int main(int argc, char** argv) { if (cpplogEnabled(cpplogging::debug) && opt.tabled) { p.printTabledSequents(std::cerr); } - + + // Print Vacuity output. + // First, print which formulas were checked + if(!HIDE_VACUITY_OUTPUT){ + std::cout << "Checking with Full Vacuity is " << opt.allVacuity << std::endl; + std::cout << "\n====Equation Expressions (**u** expressions unchecked):" << std::endl; + for(std::map::const_iterator it = input_pes.equations().begin(); + it != input_pes.equations().end(); ++it) { + ExprNode *ls = (*it).second; + + std::cout << (*it).first; + if(ls->get_Parity()) { + std::cout << " :nu= "; + } + else { + std::cout << " :mu= "; + } + ls->printExamined(std::cout); + std::cout << std::endl; + } + } + + // Now print what formulas are vacuous or not + if(!HIDE_VACUITY_OUTPUT) { + // Do Extra Work to delete Dynamically Allocated Elements + std::cout << "\n====Equation Expressions (*--v--* expressions vacuous):" << std::endl; + for(std::map::const_iterator it = input_pes.equations().begin(); + it != input_pes.equations().end(); ++it) { + ExprNode *ls = (*it).second; + + std::cout << (*it).first; + if(ls->get_Parity()) { + std::cout << " :nu= "; + } + else { + std::cout << " :mu= "; + } + ls->printDetectVacuous(std::cout, suc); + std::cout << std::endl; + } + } + cpplog(cpplogging::info) << "==--End of Program Execution-----------------------==" << std::endl; diff --git a/pes.timed/transition.hh b/pes.timed/transition.hh index 54bed0c..ade0a00 100644 --- a/pes.timed/transition.hh +++ b/pes.timed/transition.hh @@ -94,7 +94,7 @@ public: * the destination (state change) of the transition. * @return The ExprNode describing the destination (state change) of the * transition. */ - const ExprNode* getRightExpr() const { return rightExpr; } + ExprNode* getRightExpr() const { return rightExpr; } /** Retrieve the list of clock assignments stored by this transition. * @return the vector containing the ordered list of clock assignments From 3df2a5ef4f4ab826c797c477d3e4a34f8ad39604 Mon Sep 17 00:00:00 2001 From: Peter Fontana Date: Sun, 2 Feb 2020 19:47:44 -0500 Subject: [PATCH 03/11] Modified .gitignore --- .DS_Store | Bin 10244 -> 0 bytes .gitignore | 1 + 2 files changed, 1 insertion(+) delete mode 100644 .DS_Store diff --git a/.DS_Store b/.DS_Store deleted file mode 100644 index f134e5ba599dde098fb024579c7068ca5111cba3..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 10244 zcmeHMPfr_16n|rrVut|Bzowv8vOtll29O;hq*RJx3?xNL0>u`^C8@Kv7qiNG*VwkVPck&Yzx?kTtWQ4Dw{vs)kj?o6^G@SHuX!2*e1)2*e1)2wV*W zuxIm>8uDnI#|Xp-#0XpnV6FX@6`d^WR*fnsq!DmoC$Vnfg{Z=$*^~h<-ZvwwoTZZnq+3asDksP@8 z&R{By-*D=A@xVGNx~kiD3aY)w-?miupeoBH%Q7y?YIR4~jw;IJs%5&WZfdp=*6SKr zo_(g9b?c~LwavOC^c1}YZYNz)rcY0omvZx&J4?B<`OIl9dv9qzb9edP*;zVu^H%Qu z#*1d>8|*=HF(j+_ zWY@@oM2Ggpyz_DNtP?)_jQM7NCPKae>n5!s-$!rS7>kQ>^&JlZm4MFcKAjI`U!34L z*my|BkHKTea2&bK2n@JvU={{pZyM(cE3tf7NSf80^&=MG9 zlIlRa7P9qc$d=@KYyC=&FXU4xpnHs!(}Xt}9O)oRB3AjmsE7ZG;dLjQozLW!|A#o# zGtv-p3N^5*EaV(FSFX~9ezBZky#-d~L?3y+R*&G*2B;d|5%_!rw2bu8;*cF)@jR9V zWRtL=Q#Cl_JZc5FhUhVTb(PlPuSMjMelFrp(Rohn0hF0i2H`JzY*?{=JF4_ zg^#>~LUUe$Hy{$Yb` zn$5D?>@K^{9^q5xwKFG$4W3IK>FW2*e0n2?UZ}FEaf5|9b!b|F1+}<4(i~#0b0| z1lYh@ajgK|-NRqlOac`dJTLI@#QDxWDnyWR7G5tt$K!>6j{i{BWjW;u?RiPhJu1Xe hFT_E;ulcY2&ww}m9WuWE^KWGf_+l2{|KHGB{0}K(+hPC! diff --git a/.gitignore b/.gitignore index 3d7a28d..1338d88 100644 --- a/.gitignore +++ b/.gitignore @@ -58,3 +58,4 @@ pes.timed/test/dbmtest[1]_include.cmake pes.timed/test/parsetest[1]_include.cmake pes.timed/test/prooftest[1]_include.cmake Doxyfile.doxygen +.DS_Store \ No newline at end of file From 1f656c244e9e880d0d44fa64a1edd891227059ef Mon Sep 17 00:00:00 2001 From: Peter Fontana Date: Sun, 2 Feb 2020 19:47:58 -0500 Subject: [PATCH 04/11] Removed const changes for debugging purposes. --- pes.timed/ExprNode.hh | 2 +- pes.timed/proof.hh | 185 +++++++++++++++++++------------------ pes.timed/timesolver-ta.cc | 1 - 3 files changed, 94 insertions(+), 94 deletions(-) diff --git a/pes.timed/ExprNode.hh b/pes.timed/ExprNode.hh index b7baecc..8a72f37 100644 --- a/pes.timed/ExprNode.hh +++ b/pes.timed/ExprNode.hh @@ -899,7 +899,7 @@ public: /** Records whether this expression was examined by * the PES prover. * @param newVal the boolean value to record. */ - void setExaminedDuringProof(bool newVal) { + void setExaminedDuringProof(bool newVal){ examinedDuringProof = newVal; } diff --git a/pes.timed/proof.hh b/pes.timed/proof.hh index 88b27a2..987b642 100644 --- a/pes.timed/proof.hh +++ b/pes.timed/proof.hh @@ -114,7 +114,7 @@ protected: __attribute__((flatten)) bool do_proof(const SubstList& discrete_state, const DBM& zone, - ExprNode& formula) { + const ExprNode& formula) { assert(zone.isInCf()); bool result = false; if (cpplogEnabled(cpplogging::debug)) { @@ -124,7 +124,7 @@ protected: ++step; if(!options.allVacuity) { - formula.setExaminedDuringProof(true); + // formula.setExaminedDuringProof(true); } switch (formula.getOpType()) { @@ -231,10 +231,10 @@ protected: } if(!options.allVacuity) { if(result) { - //formula.getRight()->setValidDuringProof(true); + // formula.setValidDuringProof(true); } else { - //formula.getRight()->setInvalidDuringProof(true); + // formula.setInvalidDuringProof(true); } } --step; @@ -260,7 +260,7 @@ protected: * and the return value. */ __attribute__((flatten)) void do_proof_place(const SubstList& discrete_state, const DBM& zone, DBMList* place, - ExprNode& formula) { + const ExprNode& formula) { /* do_proof_place() written by Peter Fontana, needed for support * of EXISTS Quantifiers. */ assert(zone.isInCf()); @@ -272,7 +272,7 @@ protected: } if(!options.allVacuity) { - formula.setExaminedDuringProof(true); + // formula.setExaminedDuringProof(true); } ++step; @@ -380,10 +380,10 @@ protected: } if(!options.allVacuity) { if( (place!=NULL) & !(place->emptiness())) { - //formula.getRight()->setValidDuringProof(true); + // formula.setValidDuringProof(true); } else { - //formula.getRight()->setInvalidDuringProof(true); + // formula.setInvalidDuringProof(true); } } @@ -391,97 +391,97 @@ protected: } bool do_proof_predicate(const SubstList& discrete_state, const DBM& zone, - ExprNode& formula); + const ExprNode& formula); bool do_proof_and(const SubstList& discrete_state, const DBM& zone, - ExprNode& formula); + const ExprNode& formula); bool do_proof_or(const SubstList& discrete_state, const DBM& zone, - ExprNode& formula); + const ExprNode& formula); bool do_proof_or_simple(const SubstList& discrete_state, const DBM& zone, - ExprNode& formula); + const ExprNode& formula); bool do_proof_forall(const SubstList& discrete_state, const DBM& zone, - ExprNode& formula); + const ExprNode& formula); bool do_proof_forall_rel(const SubstList& discrete_state, const DBM& zone, - ExprNode& formula); + const ExprNode& formula); bool do_proof_exists(const SubstList& discrete_state, const DBM& zone, - ExprNode& formula); + const ExprNode& formula); bool do_proof_exists_rel(const SubstList& discrete_state, const DBM& zone, - ExprNode& formula); + const ExprNode& formula); bool do_proof_allact(const SubstList& discrete_state, const DBM& zone, - ExprNode& formula); + const ExprNode& formula); bool do_proof_existact(const SubstList& discrete_state, const DBM& zone, - ExprNode& formula); + const ExprNode& formula); bool do_proof_imply(const SubstList& discrete_state, const DBM& zone, - ExprNode& formula); - bool do_proof_constraint(const DBM& zone, ExprNode& formula) const; + const ExprNode& formula); + bool do_proof_constraint(const DBM& zone, const ExprNode& formula) const; bool do_proof_sublist(const SubstList& discrete_state, const DBM& zone, - ExprNode& formula); + const ExprNode& formula); bool do_proof_reset(const SubstList& discrete_state, const DBM& zone, - ExprNode& formula); + const ExprNode& formula); bool do_proof_assign(const SubstList& discrete_state, const DBM& zone, - ExprNode& formula); + const ExprNode& formula); bool do_proof_replace(const SubstList& discrete_state, const DBM& zone, - ExprNode& formula); + const ExprNode& formula); void do_proof_place_predicate(const SubstList& discrete_state, const DBM& zone, DBMList* place, - ExprNode& formula); + const ExprNode& formula); void do_proof_place_and(const SubstList& discrete_state, const DBM& zone, DBMList* place, - ExprNode& formula); + const ExprNode& formula); void do_proof_place_or(const SubstList& discrete_state, const DBM& zone, DBMList* place, - ExprNode& formula); + const ExprNode& formula); void do_proof_place_or_simple(const SubstList& discrete_state, const DBM& zone, DBMList* place, - ExprNode& formula); + const ExprNode& formula); void do_proof_place_forall(const SubstList& discrete_state, const DBM& zone, DBMList* place, - ExprNode& formula); + const ExprNode& formula); void do_proof_place_forall_rel(const SubstList& discrete_state, const DBM& zone, DBMList* place, - ExprNode& formula); + const ExprNode& formula); void do_proof_place_exists(const SubstList& discrete_state, const DBM& zone, DBMList* place, - ExprNode& formula); + const ExprNode& formula); void do_proof_place_exists_rel(const SubstList& discrete_state, const DBM& zone, DBMList* place, - ExprNode& formula); + const ExprNode& formula); void do_proof_place_allact(const SubstList& discrete_state, const DBM& zone, DBMList* place, - ExprNode& formula); + const ExprNode& formula); void do_proof_place_existact(const SubstList& discrete_state, const DBM& zone, DBMList* place, - ExprNode& formula); + const ExprNode& formula); void do_proof_place_imply(const SubstList& discrete_state, const DBM& zone, DBMList* place, - ExprNode& formula); + const ExprNode& formula); void do_proof_place_constraint(const DBM& zone, DBMList* place, - ExprNode& formula) const; - bool do_proof_place_bool(DBMList* place, ExprNode& formula) const; + const ExprNode& formula) const; + bool do_proof_place_bool(DBMList* place, const ExprNode& formula) const; bool do_proof_place_atomic(const SubstList& discrete_state, - DBMList* place, ExprNode& formula) const; + DBMList* place, const ExprNode& formula) const; bool do_proof_place_atomic_not(const SubstList& discrete_state, - DBMList* place, ExprNode& formula) const; + DBMList* place, const ExprNode& formula) const; bool do_proof_place_atomic_lt(const SubstList& discrete_state, - DBMList* place, ExprNode& formula) const; + DBMList* place, const ExprNode& formula) const; bool do_proof_place_atomic_gt(const SubstList& discrete_state, - DBMList* place, ExprNode& formula) const; + DBMList* place, const ExprNode& formula) const; bool do_proof_place_atomic_le(const SubstList& discrete_state, - DBMList* place, ExprNode& formula) const; + DBMList* place, const ExprNode& formula) const; bool do_proof_place_atomic_ge(const SubstList& discrete_state, - DBMList* place, ExprNode& formula) const; + DBMList* place, const ExprNode& formula) const; void do_proof_place_sublist(const SubstList& discrete_state, const DBM& zone, DBMList* place, - ExprNode& formula); + const ExprNode& formula); void do_proof_place_reset(const SubstList& discrete_state, const DBM& zone, DBMList* place, - ExprNode& formula); + const ExprNode& formula); void do_proof_place_assign(const SubstList& discrete_state, const DBM& zone, DBMList* place, - ExprNode& formula); + const ExprNode& formula); void do_proof_place_replace(const SubstList& discrete_state, const DBM& zone, DBMList* place, - ExprNode& formula); + const ExprNode& formula); bool do_proof_place_ablewaitinf(const SubstList& discrete_state, const DBM& zone, DBMList* place) const; bool do_proof_place_unablewaitinf(const SubstList& discrete_state, @@ -674,7 +674,7 @@ protected: /* IMPLEMENTATION PROOF WITHOUT PLACEHOLDERS */ inline bool prover::do_proof_predicate(const SubstList& discrete_state, const DBM& zone, - ExprNode& formula) { + const ExprNode& formula) { bool retVal = false; /* Look in Known True and Known False Sequent Caches */ @@ -774,7 +774,7 @@ inline bool prover::do_proof_predicate(const SubstList& discrete_state, // [FC14] Proof rule \land inline bool prover::do_proof_and(const SubstList& discrete_state, - const DBM& zone, ExprNode& formula) { + const DBM& zone, const ExprNode& formula) { /* Because zone is only changed after it is copied, it can * be passed to both branches. */ bool retVal = do_proof(discrete_state, zone, *formula.getLeft()); @@ -791,7 +791,7 @@ inline bool prover::do_proof_and(const SubstList& discrete_state, */ // [FC14] Proof rule based on \lor_{s_2} inline bool prover::do_proof_or(const SubstList& discrete_state, - const DBM& zone, ExprNode& formula) { + const DBM& zone, const ExprNode& formula) { bool retVal = false; /* Use two placeholders to provide split here */ @@ -831,7 +831,7 @@ inline bool prover::do_proof_or(const SubstList& discrete_state, // [FC14], rules \lor_{l} and \lor_{r} inline bool prover::do_proof_or_simple(const SubstList& discrete_state, const DBM& zone, - ExprNode& formula) { + const ExprNode& formula) { /* Simplified OR does not need to split on placeholders */ bool retVal = do_proof(discrete_state, zone, *formula.getLeft()); if (!retVal) { @@ -842,7 +842,7 @@ inline bool prover::do_proof_or_simple(const SubstList& discrete_state, // [FC14] Rule \forall_{t1} inline bool prover::do_proof_forall(const SubstList& discrete_state, - const DBM& zone, ExprNode& formula) { + const DBM& zone, const ExprNode& formula) { /* Here the model checker looks at the zone of * all time sucessors and then substitutes in * the substitued constraints and sees if the @@ -864,7 +864,7 @@ inline bool prover::do_proof_forall(const SubstList& discrete_state, // [FC14] Proof rules \forall_{ro1}, \forall_{ro2}, \forall_{ro3} inline bool prover::do_proof_forall_rel(const SubstList& discrete_state, const DBM& zone, - ExprNode& formula) { + const ExprNode& formula) { /* Proof methodology: * first, see if \phi_1 is satisfied during the time advance. @@ -1040,7 +1040,7 @@ inline bool prover::do_proof_forall_rel(const SubstList& discrete_state, // [FC14] Proof rule \exists_{t1} inline bool prover::do_proof_exists(const SubstList& discrete_state, - const DBM& zone, ExprNode& formula) { + const DBM& zone, const ExprNode& formula) { /* Support for exists(), written by Peter Fontana */ // This support gives a placeholder variable // and uses a similar method do_proof_place @@ -1092,7 +1092,7 @@ inline bool prover::do_proof_exists(const SubstList& discrete_state, inline bool prover::do_proof_exists_rel(const SubstList& discrete_state, const DBM& zone, - ExprNode& formula) { + const ExprNode& formula) { bool retVal = false; /* First Try to get a placeholder value that works */ @@ -1275,7 +1275,7 @@ inline bool prover::do_proof_exists_rel(const SubstList& discrete_state, } inline bool prover::do_proof_allact(const SubstList& discrete_state, - const DBM& zone, ExprNode& formula) { + const DBM& zone, const ExprNode& formula) { bool retVal = true; /* Enumerate through all transitions */ cpplog(cpplogging::debug) << "\t Proving ALLACT Transitions:----\n" @@ -1370,7 +1370,7 @@ inline bool prover::do_proof_allact(const SubstList& discrete_state, inline bool prover::do_proof_existact(const SubstList& discrete_state, const DBM& zone, - ExprNode& formula) { + const ExprNode& formula) { bool retVal = false; /* Enumerate through all transitions */ @@ -1478,7 +1478,7 @@ inline bool prover::do_proof_existact(const SubstList& discrete_state, } inline bool prover::do_proof_imply(const SubstList& discrete_state, - const DBM& zone, ExprNode& formula) { + const DBM& zone, const ExprNode& formula) { bool retVal = false; /* Here is the one call to comp_ph(...) outside of comp_ph(...) */ DBM zone_lhs(zone); @@ -1506,7 +1506,7 @@ inline bool prover::do_proof_imply(const SubstList& discrete_state, } inline bool prover::do_proof_constraint(const DBM& zone, - ExprNode& formula) const { + const ExprNode& formula) const { bool retVal = (zone <= *(formula.dbm())); cpplog(cpplogging::debug) << "---(" << (retVal ? "V" : "Inv") @@ -1516,13 +1516,13 @@ inline bool prover::do_proof_constraint(const DBM& zone, } inline bool prover::do_proof_sublist(const SubstList& discrete_state, - const DBM& zone, ExprNode& formula) { + const DBM& zone, const ExprNode& formula) { SubstList st(formula.getSublist(), &discrete_state); return do_proof(st, zone, *formula.getExpr()); } inline bool prover::do_proof_reset(const SubstList& discrete_state, - const DBM& zone, ExprNode& formula) { + const DBM& zone, const ExprNode& formula) { DBM lhs_reset(zone); lhs_reset.reset(*formula.getClockSet()); lhs_reset.cf(); @@ -1530,7 +1530,7 @@ inline bool prover::do_proof_reset(const SubstList& discrete_state, } inline bool prover::do_proof_assign(const SubstList& discrete_state, - const DBM& zone, ExprNode& formula) { + const DBM& zone, const ExprNode& formula) { // Formula is phi[x:=y] with x and y clocks. DBM lhs_assign(zone); lhs_assign.reset(formula.getcX(), formula.getcY()); @@ -1539,7 +1539,7 @@ inline bool prover::do_proof_assign(const SubstList& discrete_state, } inline bool prover::do_proof_replace(const SubstList& discrete_state, - const DBM& zone, ExprNode& formula) { + const DBM& zone, const ExprNode& formula) { SubstList sub_(discrete_state); sub_[formula.getcX()] = discrete_state.at(formula.getcY()); return do_proof(sub_, zone, *formula.getExpr()); @@ -1548,7 +1548,7 @@ inline bool prover::do_proof_replace(const SubstList& discrete_state, /* IMPLEMENTATION PROVER WITH PLACEHOLDERS */ inline void prover::do_proof_place_predicate(const SubstList& discrete_state, const DBM& zone, DBMList* place, - ExprNode& formula) { + const ExprNode& formula) { ExprNode* e = input_pes.lookup_equation(formula.getPredicate()); /* First look in known true and false sequent tables */ @@ -1657,7 +1657,7 @@ inline void prover::do_proof_place_predicate(const SubstList& discrete_state, inline void prover::do_proof_place_and(const SubstList& discrete_state, const DBM& zone, DBMList* place, - ExprNode& formula) { + const ExprNode& formula) { DBMList currPlace(*place); do_proof_place(discrete_state, zone, place, *formula.getLeft()); place->cf(); @@ -1665,7 +1665,7 @@ inline void prover::do_proof_place_and(const SubstList& discrete_state, /* for vacuity reasons, send the largest placeholder possible; * hence only pass the intersected one if there is no vacuity. */ if(!options.allVacuity) { - place->intersect(currPlace); + //place->intersect(currPlace); } do_proof_place(discrete_state, zone, place, *formula.getRight()); } @@ -1675,12 +1675,12 @@ inline void prover::do_proof_place_and(const SubstList& discrete_state, // [FC14] Proof rule \lor_{s2} inline void prover::do_proof_place_or(const SubstList& discrete_state, const DBM& zone, DBMList* place, - ExprNode& formula) { + const ExprNode& formula) { DBMList placeholder_left(*place); do_proof_place(discrete_state, zone, &placeholder_left, *formula.getLeft()); placeholder_left.cf(); - + // bool emptyLeft = placeholder_left.emptiness(); if (!(placeholder_left >= *place)) { // We use place here, since the result of the second call is likely to be @@ -1697,9 +1697,7 @@ inline void prover::do_proof_place_or(const SubstList& discrete_state, << "Left Placeholder of OR (P): " << placeholder_left << "\nRight Placeholder of OR (P): " << *place << std::endl; } - else if (!options.allVacuity) { - formula.getRight()->setBypassedDuringProof(true); - } + place->union_(placeholder_left); place->cf(); @@ -1708,12 +1706,15 @@ inline void prover::do_proof_place_or(const SubstList& discrete_state, << "Final Placeholder of OR (P): " << *place << std::endl << std::endl; } + else if (!options.allVacuity) { + // formula.getRight()->setBypassedDuringProof(true); + } } inline void prover::do_proof_place_or_simple(const SubstList& discrete_state, const DBM& zone, DBMList* place, - ExprNode& formula) { + const ExprNode& formula) { /* In OR_SIMPLE, the placeholder will either be empty or completely full * in one of the two cases. Hence, fewer comparisons with unions of zones * are needed. */ @@ -1741,7 +1742,7 @@ inline void prover::do_proof_place_or_simple(const SubstList& discrete_state, } } else if (!options.allVacuity) { - formula.getRight()->setBypassedDuringProof(true); + // formula.getRight()->setBypassedDuringProof(true); } @@ -1751,7 +1752,7 @@ inline void prover::do_proof_place_or_simple(const SubstList& discrete_state, inline void prover::do_proof_place_forall(const SubstList& discrete_state, const DBM& zone, DBMList* place, - ExprNode& formula) { + const ExprNode& formula) { /* Here the model checker looks at the zone of * all time sucessors and then substitutes in * the substitued constraints and sees if the @@ -1807,7 +1808,7 @@ inline void prover::do_proof_place_forall(const SubstList& discrete_state, inline void prover::do_proof_place_forall_rel(const SubstList& discrete_state, const DBM& zone, DBMList* place, - ExprNode& formula) { + const ExprNode& formula) { /* Proof methodology: * first, see if \phi_1 is satisfied during the time advance. * If it is, check that phi_2 is true both at and before those @@ -2014,7 +2015,7 @@ inline void prover::do_proof_place_forall_rel(const SubstList& discrete_state, inline void prover::do_proof_place_exists(const SubstList& discrete_state, const DBM& zone, DBMList* place, - ExprNode& formula) { + const ExprNode& formula) { /* First try to get a new placeholder value that works */ DBM lhs_succ(zone); lhs_succ.suc(); @@ -2067,7 +2068,7 @@ inline void prover::do_proof_place_exists(const SubstList& discrete_state, inline void prover::do_proof_place_exists_rel(const SubstList& discrete_state, const DBM& zone, DBMList* place, - ExprNode& formula) { + const ExprNode& formula) { /* First Try to get a placeholder value that works */ DBM zone_succ(zone); zone_succ.suc(); @@ -2225,7 +2226,7 @@ inline void prover::do_proof_place_exists_rel(const SubstList& discrete_state, inline void prover::do_proof_place_allact(const SubstList& discrete_state, const DBM& zone, DBMList* place, - ExprNode& formula) { + const ExprNode& formula) { /* Enumerate through all transitions */ cpplog(cpplogging::debug) << "\t Proving ALLACT Transitions:----\n" << std::endl; @@ -2344,7 +2345,7 @@ inline void prover::do_proof_place_allact(const SubstList& discrete_state, inline void prover::do_proof_place_existact(const SubstList& discrete_state, const DBM& zone, DBMList* place, - ExprNode& formula) { + const ExprNode& formula) { DBMList result(INFTYDBM); // DBM to accumulate the result. result.makeEmpty(); @@ -2446,7 +2447,7 @@ inline void prover::do_proof_place_existact(const SubstList& discrete_state, inline void prover::do_proof_place_imply(const SubstList& discrete_state, const DBM& zone, DBMList* place, - ExprNode& formula) { + const ExprNode& formula) { DBM zone_copy(zone); /* call comp_ph() for efficient proving of IMPLY's left. */ if (comp_ph(zone_copy, *(formula.getLeft()), discrete_state)) { @@ -2471,7 +2472,7 @@ inline void prover::do_proof_place_imply(const SubstList& discrete_state, inline void prover::do_proof_place_constraint(const DBM& zone, DBMList* place, - ExprNode& formula) const { + const ExprNode& formula) const { if (zone <= *(formula.dbm())) { cpplog(cpplogging::debug) << "---(Valid) Leaf DBM (CONSTRAINT) Reached " "with no need for Placeholder----" @@ -2513,7 +2514,7 @@ inline void prover::do_proof_place_constraint(const DBM& zone, } inline bool prover::do_proof_place_bool(DBMList* place, - ExprNode& formula) const { + const ExprNode& formula) const { bool retVal = (formula.getBool()); cpplog(cpplogging::debug) << "---(" << (retVal ? "V" : "Inv") << "alid) Leaf BOOL Reached----" << std::endl @@ -2528,7 +2529,7 @@ inline bool prover::do_proof_place_bool(DBMList* place, inline bool prover::do_proof_place_atomic(const SubstList& discrete_state, DBMList* place, - ExprNode& formula) const { + const ExprNode& formula) const { bool retVal = (discrete_state.at(formula.getAtomic()) == formula.getIntVal()); cpplog(cpplogging::debug) << "---(" << (retVal ? "V" : "Inv") << "alid) Leaf ATOMIC == Reached----" << std::endl @@ -2542,7 +2543,7 @@ inline bool prover::do_proof_place_atomic(const SubstList& discrete_state, inline bool prover::do_proof_place_atomic_not(const SubstList& discrete_state, DBMList* place, - ExprNode& formula) const { + const ExprNode& formula) const { bool retVal = (discrete_state.at(formula.getAtomic()) != formula.getIntVal()); cpplog(cpplogging::debug) << "---(" << (retVal ? "V" : "Inv") << "alid) Leaf ATOMIC != Reached----" << std::endl @@ -2557,7 +2558,7 @@ inline bool prover::do_proof_place_atomic_not(const SubstList& discrete_state, inline bool prover::do_proof_place_atomic_lt(const SubstList& discrete_state, DBMList* place, - ExprNode& formula) const { + const ExprNode& formula) const { bool retVal = (discrete_state.at(formula.getAtomic()) < formula.getIntVal()); cpplog(cpplogging::debug) << "---(" << (retVal ? "V" : "Inv") << "alid) Leaf ATOMIC < Reached----" << std::endl @@ -2572,7 +2573,7 @@ inline bool prover::do_proof_place_atomic_lt(const SubstList& discrete_state, inline bool prover::do_proof_place_atomic_gt(const SubstList& discrete_state, DBMList* place, - ExprNode& formula) const { + const ExprNode& formula) const { bool retVal = (discrete_state.at(formula.getAtomic()) > formula.getIntVal()); cpplog(cpplogging::debug) << "---(" << (retVal ? "V" : "Inv") << "alid) Leaf ATOMIC > Reached----" << std::endl @@ -2585,7 +2586,7 @@ inline bool prover::do_proof_place_atomic_gt(const SubstList& discrete_state, inline bool prover::do_proof_place_atomic_le(const SubstList& discrete_state, DBMList* place, - ExprNode& formula) const { + const ExprNode& formula) const { bool retVal = (discrete_state.at(formula.getAtomic()) <= formula.getIntVal()); cpplog(cpplogging::debug) << "---(" << (retVal ? "V" : "Inv") << "alid) Leaf ATOMIC < Reached----" << std::endl @@ -2600,7 +2601,7 @@ inline bool prover::do_proof_place_atomic_le(const SubstList& discrete_state, inline bool prover::do_proof_place_atomic_ge(const SubstList& discrete_state, DBMList* place, - ExprNode& formula) const { + const ExprNode& formula) const { bool retVal = (discrete_state.at(formula.getAtomic()) >= formula.getIntVal()); cpplog(cpplogging::debug) << "---(" << (retVal ? "V" : "Inv") << "alid) Leaf ATOMIC > Reached----" << std::endl @@ -2615,7 +2616,7 @@ inline bool prover::do_proof_place_atomic_ge(const SubstList& discrete_state, inline void prover::do_proof_place_sublist(const SubstList& discrete_state, const DBM& zone, DBMList* place, - ExprNode& formula) { + const ExprNode& formula) { SubstList st(formula.getSublist(), &discrete_state); do_proof_place(st, zone, place, *formula.getExpr()); } @@ -2623,7 +2624,7 @@ inline void prover::do_proof_place_sublist(const SubstList& discrete_state, inline void prover::do_proof_place_reset(const SubstList& discrete_state, const DBM& zone, DBMList* place, - ExprNode& formula) { + const ExprNode& formula) { DBM lhs_reset(zone); // JK: It does not become clear why this is necessary here // lhs_reset.bound(input_pes.max_constant()); @@ -2665,7 +2666,7 @@ inline void prover::do_proof_place_reset(const SubstList& discrete_state, inline void prover::do_proof_place_assign(const SubstList& discrete_state, const DBM& zone, DBMList* place, - ExprNode& formula) { + const ExprNode& formula) { DBM lhs_assign(zone); /* Here the DBM zone is where the value of * clock x is reset to clock y, which is possibly @@ -2708,7 +2709,7 @@ inline void prover::do_proof_place_assign(const SubstList& discrete_state, inline void prover::do_proof_place_replace(const SubstList& discrete_state, const DBM& zone, DBMList* place, - ExprNode& formula) { + const ExprNode& formula) { SubstList sub_(discrete_state); sub_[formula.getcX()] = discrete_state.at(formula.getcY()); do_proof_place(sub_, zone, place, *formula.getExpr()); diff --git a/pes.timed/timesolver-ta.cc b/pes.timed/timesolver-ta.cc index 6821761..32a042e 100644 --- a/pes.timed/timesolver-ta.cc +++ b/pes.timed/timesolver-ta.cc @@ -328,7 +328,6 @@ int main(int argc, char** argv) { // Now print what formulas are vacuous or not if(!HIDE_VACUITY_OUTPUT) { - // Do Extra Work to delete Dynamically Allocated Elements std::cout << "\n====Equation Expressions (*--v--* expressions vacuous):" << std::endl; for(std::map::const_iterator it = input_pes.equations().begin(); it != input_pes.equations().end(); ++it) { From cc130b4bb52b4aca71fc55ccc3de575a87292a04 Mon Sep 17 00:00:00 2001 From: Peter Fontana Date: Sun, 2 Feb 2020 20:32:54 -0500 Subject: [PATCH 05/11] Modified Simple Vacuity Checking to pass tests --- pes.timed/proof.hh | 181 +++++++++++++++++++++++---------------------- 1 file changed, 92 insertions(+), 89 deletions(-) diff --git a/pes.timed/proof.hh b/pes.timed/proof.hh index 987b642..e9b01b8 100644 --- a/pes.timed/proof.hh +++ b/pes.timed/proof.hh @@ -114,7 +114,7 @@ protected: __attribute__((flatten)) bool do_proof(const SubstList& discrete_state, const DBM& zone, - const ExprNode& formula) { + ExprNode& formula) { assert(zone.isInCf()); bool result = false; if (cpplogEnabled(cpplogging::debug)) { @@ -124,7 +124,7 @@ protected: ++step; if(!options.allVacuity) { - // formula.setExaminedDuringProof(true); + formula.setExaminedDuringProof(true); } switch (formula.getOpType()) { @@ -231,10 +231,10 @@ protected: } if(!options.allVacuity) { if(result) { - // formula.setValidDuringProof(true); + formula.setValidDuringProof(true); } else { - // formula.setInvalidDuringProof(true); + formula.setInvalidDuringProof(true); } } --step; @@ -260,7 +260,7 @@ protected: * and the return value. */ __attribute__((flatten)) void do_proof_place(const SubstList& discrete_state, const DBM& zone, DBMList* place, - const ExprNode& formula) { + ExprNode& formula) { /* do_proof_place() written by Peter Fontana, needed for support * of EXISTS Quantifiers. */ assert(zone.isInCf()); @@ -272,7 +272,7 @@ protected: } if(!options.allVacuity) { - // formula.setExaminedDuringProof(true); + formula.setExaminedDuringProof(true); } ++step; @@ -379,11 +379,14 @@ protected: } } if(!options.allVacuity) { - if( (place!=NULL) & !(place->emptiness())) { - // formula.setValidDuringProof(true); + if(place!=NULL) { + place->cf(); + if(!(place->emptiness())) { + formula.setValidDuringProof(true); + } } else { - // formula.setInvalidDuringProof(true); + formula.setInvalidDuringProof(true); } } @@ -391,97 +394,97 @@ protected: } bool do_proof_predicate(const SubstList& discrete_state, const DBM& zone, - const ExprNode& formula); + ExprNode& formula); bool do_proof_and(const SubstList& discrete_state, const DBM& zone, - const ExprNode& formula); + ExprNode& formula); bool do_proof_or(const SubstList& discrete_state, const DBM& zone, - const ExprNode& formula); + ExprNode& formula); bool do_proof_or_simple(const SubstList& discrete_state, const DBM& zone, - const ExprNode& formula); + ExprNode& formula); bool do_proof_forall(const SubstList& discrete_state, const DBM& zone, - const ExprNode& formula); + ExprNode& formula); bool do_proof_forall_rel(const SubstList& discrete_state, const DBM& zone, - const ExprNode& formula); + ExprNode& formula); bool do_proof_exists(const SubstList& discrete_state, const DBM& zone, - const ExprNode& formula); + ExprNode& formula); bool do_proof_exists_rel(const SubstList& discrete_state, const DBM& zone, - const ExprNode& formula); + ExprNode& formula); bool do_proof_allact(const SubstList& discrete_state, const DBM& zone, - const ExprNode& formula); + ExprNode& formula); bool do_proof_existact(const SubstList& discrete_state, const DBM& zone, - const ExprNode& formula); + ExprNode& formula); bool do_proof_imply(const SubstList& discrete_state, const DBM& zone, - const ExprNode& formula); - bool do_proof_constraint(const DBM& zone, const ExprNode& formula) const; + ExprNode& formula); + bool do_proof_constraint(const DBM& zone, ExprNode& formula) const; bool do_proof_sublist(const SubstList& discrete_state, const DBM& zone, - const ExprNode& formula); + ExprNode& formula); bool do_proof_reset(const SubstList& discrete_state, const DBM& zone, - const ExprNode& formula); + ExprNode& formula); bool do_proof_assign(const SubstList& discrete_state, const DBM& zone, - const ExprNode& formula); + ExprNode& formula); bool do_proof_replace(const SubstList& discrete_state, const DBM& zone, - const ExprNode& formula); + ExprNode& formula); void do_proof_place_predicate(const SubstList& discrete_state, const DBM& zone, DBMList* place, - const ExprNode& formula); + ExprNode& formula); void do_proof_place_and(const SubstList& discrete_state, const DBM& zone, DBMList* place, - const ExprNode& formula); + ExprNode& formula); void do_proof_place_or(const SubstList& discrete_state, const DBM& zone, DBMList* place, - const ExprNode& formula); + ExprNode& formula); void do_proof_place_or_simple(const SubstList& discrete_state, const DBM& zone, DBMList* place, - const ExprNode& formula); + ExprNode& formula); void do_proof_place_forall(const SubstList& discrete_state, const DBM& zone, DBMList* place, - const ExprNode& formula); + ExprNode& formula); void do_proof_place_forall_rel(const SubstList& discrete_state, const DBM& zone, DBMList* place, - const ExprNode& formula); + ExprNode& formula); void do_proof_place_exists(const SubstList& discrete_state, const DBM& zone, DBMList* place, - const ExprNode& formula); + ExprNode& formula); void do_proof_place_exists_rel(const SubstList& discrete_state, const DBM& zone, DBMList* place, - const ExprNode& formula); + ExprNode& formula); void do_proof_place_allact(const SubstList& discrete_state, const DBM& zone, DBMList* place, - const ExprNode& formula); + ExprNode& formula); void do_proof_place_existact(const SubstList& discrete_state, const DBM& zone, DBMList* place, - const ExprNode& formula); + ExprNode& formula); void do_proof_place_imply(const SubstList& discrete_state, const DBM& zone, DBMList* place, - const ExprNode& formula); + ExprNode& formula); void do_proof_place_constraint(const DBM& zone, DBMList* place, - const ExprNode& formula) const; - bool do_proof_place_bool(DBMList* place, const ExprNode& formula) const; + ExprNode& formula) const; + bool do_proof_place_bool(DBMList* place, ExprNode& formula) const; bool do_proof_place_atomic(const SubstList& discrete_state, - DBMList* place, const ExprNode& formula) const; + DBMList* place, ExprNode& formula) const; bool do_proof_place_atomic_not(const SubstList& discrete_state, - DBMList* place, const ExprNode& formula) const; + DBMList* place, ExprNode& formula) const; bool do_proof_place_atomic_lt(const SubstList& discrete_state, - DBMList* place, const ExprNode& formula) const; + DBMList* place, ExprNode& formula) const; bool do_proof_place_atomic_gt(const SubstList& discrete_state, - DBMList* place, const ExprNode& formula) const; + DBMList* place, ExprNode& formula) const; bool do_proof_place_atomic_le(const SubstList& discrete_state, - DBMList* place, const ExprNode& formula) const; + DBMList* place, ExprNode& formula) const; bool do_proof_place_atomic_ge(const SubstList& discrete_state, - DBMList* place, const ExprNode& formula) const; + DBMList* place, ExprNode& formula) const; void do_proof_place_sublist(const SubstList& discrete_state, const DBM& zone, DBMList* place, - const ExprNode& formula); + ExprNode& formula); void do_proof_place_reset(const SubstList& discrete_state, const DBM& zone, DBMList* place, - const ExprNode& formula); + ExprNode& formula); void do_proof_place_assign(const SubstList& discrete_state, const DBM& zone, DBMList* place, - const ExprNode& formula); + ExprNode& formula); void do_proof_place_replace(const SubstList& discrete_state, const DBM& zone, DBMList* place, - const ExprNode& formula); + ExprNode& formula); bool do_proof_place_ablewaitinf(const SubstList& discrete_state, const DBM& zone, DBMList* place) const; bool do_proof_place_unablewaitinf(const SubstList& discrete_state, @@ -674,7 +677,7 @@ protected: /* IMPLEMENTATION PROOF WITHOUT PLACEHOLDERS */ inline bool prover::do_proof_predicate(const SubstList& discrete_state, const DBM& zone, - const ExprNode& formula) { + ExprNode& formula) { bool retVal = false; /* Look in Known True and Known False Sequent Caches */ @@ -774,7 +777,7 @@ inline bool prover::do_proof_predicate(const SubstList& discrete_state, // [FC14] Proof rule \land inline bool prover::do_proof_and(const SubstList& discrete_state, - const DBM& zone, const ExprNode& formula) { + const DBM& zone, ExprNode& formula) { /* Because zone is only changed after it is copied, it can * be passed to both branches. */ bool retVal = do_proof(discrete_state, zone, *formula.getLeft()); @@ -791,7 +794,7 @@ inline bool prover::do_proof_and(const SubstList& discrete_state, */ // [FC14] Proof rule based on \lor_{s_2} inline bool prover::do_proof_or(const SubstList& discrete_state, - const DBM& zone, const ExprNode& formula) { + const DBM& zone, ExprNode& formula) { bool retVal = false; /* Use two placeholders to provide split here */ @@ -831,7 +834,7 @@ inline bool prover::do_proof_or(const SubstList& discrete_state, // [FC14], rules \lor_{l} and \lor_{r} inline bool prover::do_proof_or_simple(const SubstList& discrete_state, const DBM& zone, - const ExprNode& formula) { + ExprNode& formula) { /* Simplified OR does not need to split on placeholders */ bool retVal = do_proof(discrete_state, zone, *formula.getLeft()); if (!retVal) { @@ -842,7 +845,7 @@ inline bool prover::do_proof_or_simple(const SubstList& discrete_state, // [FC14] Rule \forall_{t1} inline bool prover::do_proof_forall(const SubstList& discrete_state, - const DBM& zone, const ExprNode& formula) { + const DBM& zone, ExprNode& formula) { /* Here the model checker looks at the zone of * all time sucessors and then substitutes in * the substitued constraints and sees if the @@ -864,7 +867,7 @@ inline bool prover::do_proof_forall(const SubstList& discrete_state, // [FC14] Proof rules \forall_{ro1}, \forall_{ro2}, \forall_{ro3} inline bool prover::do_proof_forall_rel(const SubstList& discrete_state, const DBM& zone, - const ExprNode& formula) { + ExprNode& formula) { /* Proof methodology: * first, see if \phi_1 is satisfied during the time advance. @@ -1040,7 +1043,7 @@ inline bool prover::do_proof_forall_rel(const SubstList& discrete_state, // [FC14] Proof rule \exists_{t1} inline bool prover::do_proof_exists(const SubstList& discrete_state, - const DBM& zone, const ExprNode& formula) { + const DBM& zone, ExprNode& formula) { /* Support for exists(), written by Peter Fontana */ // This support gives a placeholder variable // and uses a similar method do_proof_place @@ -1092,7 +1095,7 @@ inline bool prover::do_proof_exists(const SubstList& discrete_state, inline bool prover::do_proof_exists_rel(const SubstList& discrete_state, const DBM& zone, - const ExprNode& formula) { + ExprNode& formula) { bool retVal = false; /* First Try to get a placeholder value that works */ @@ -1275,7 +1278,7 @@ inline bool prover::do_proof_exists_rel(const SubstList& discrete_state, } inline bool prover::do_proof_allact(const SubstList& discrete_state, - const DBM& zone, const ExprNode& formula) { + const DBM& zone, ExprNode& formula) { bool retVal = true; /* Enumerate through all transitions */ cpplog(cpplogging::debug) << "\t Proving ALLACT Transitions:----\n" @@ -1370,7 +1373,7 @@ inline bool prover::do_proof_allact(const SubstList& discrete_state, inline bool prover::do_proof_existact(const SubstList& discrete_state, const DBM& zone, - const ExprNode& formula) { + ExprNode& formula) { bool retVal = false; /* Enumerate through all transitions */ @@ -1478,7 +1481,7 @@ inline bool prover::do_proof_existact(const SubstList& discrete_state, } inline bool prover::do_proof_imply(const SubstList& discrete_state, - const DBM& zone, const ExprNode& formula) { + const DBM& zone, ExprNode& formula) { bool retVal = false; /* Here is the one call to comp_ph(...) outside of comp_ph(...) */ DBM zone_lhs(zone); @@ -1506,7 +1509,7 @@ inline bool prover::do_proof_imply(const SubstList& discrete_state, } inline bool prover::do_proof_constraint(const DBM& zone, - const ExprNode& formula) const { + ExprNode& formula) const { bool retVal = (zone <= *(formula.dbm())); cpplog(cpplogging::debug) << "---(" << (retVal ? "V" : "Inv") @@ -1516,13 +1519,13 @@ inline bool prover::do_proof_constraint(const DBM& zone, } inline bool prover::do_proof_sublist(const SubstList& discrete_state, - const DBM& zone, const ExprNode& formula) { + const DBM& zone, ExprNode& formula) { SubstList st(formula.getSublist(), &discrete_state); return do_proof(st, zone, *formula.getExpr()); } inline bool prover::do_proof_reset(const SubstList& discrete_state, - const DBM& zone, const ExprNode& formula) { + const DBM& zone, ExprNode& formula) { DBM lhs_reset(zone); lhs_reset.reset(*formula.getClockSet()); lhs_reset.cf(); @@ -1530,7 +1533,7 @@ inline bool prover::do_proof_reset(const SubstList& discrete_state, } inline bool prover::do_proof_assign(const SubstList& discrete_state, - const DBM& zone, const ExprNode& formula) { + const DBM& zone, ExprNode& formula) { // Formula is phi[x:=y] with x and y clocks. DBM lhs_assign(zone); lhs_assign.reset(formula.getcX(), formula.getcY()); @@ -1539,7 +1542,7 @@ inline bool prover::do_proof_assign(const SubstList& discrete_state, } inline bool prover::do_proof_replace(const SubstList& discrete_state, - const DBM& zone, const ExprNode& formula) { + const DBM& zone, ExprNode& formula) { SubstList sub_(discrete_state); sub_[formula.getcX()] = discrete_state.at(formula.getcY()); return do_proof(sub_, zone, *formula.getExpr()); @@ -1548,7 +1551,7 @@ inline bool prover::do_proof_replace(const SubstList& discrete_state, /* IMPLEMENTATION PROVER WITH PLACEHOLDERS */ inline void prover::do_proof_place_predicate(const SubstList& discrete_state, const DBM& zone, DBMList* place, - const ExprNode& formula) { + ExprNode& formula) { ExprNode* e = input_pes.lookup_equation(formula.getPredicate()); /* First look in known true and false sequent tables */ @@ -1657,7 +1660,7 @@ inline void prover::do_proof_place_predicate(const SubstList& discrete_state, inline void prover::do_proof_place_and(const SubstList& discrete_state, const DBM& zone, DBMList* place, - const ExprNode& formula) { + ExprNode& formula) { DBMList currPlace(*place); do_proof_place(discrete_state, zone, place, *formula.getLeft()); place->cf(); @@ -1675,7 +1678,7 @@ inline void prover::do_proof_place_and(const SubstList& discrete_state, // [FC14] Proof rule \lor_{s2} inline void prover::do_proof_place_or(const SubstList& discrete_state, const DBM& zone, DBMList* place, - const ExprNode& formula) { + ExprNode& formula) { DBMList placeholder_left(*place); do_proof_place(discrete_state, zone, &placeholder_left, *formula.getLeft()); @@ -1707,14 +1710,14 @@ inline void prover::do_proof_place_or(const SubstList& discrete_state, << std::endl; } else if (!options.allVacuity) { - // formula.getRight()->setBypassedDuringProof(true); + formula.getRight()->setBypassedDuringProof(true); } } inline void prover::do_proof_place_or_simple(const SubstList& discrete_state, const DBM& zone, DBMList* place, - const ExprNode& formula) { + ExprNode& formula) { /* In OR_SIMPLE, the placeholder will either be empty or completely full * in one of the two cases. Hence, fewer comparisons with unions of zones * are needed. */ @@ -1742,7 +1745,7 @@ inline void prover::do_proof_place_or_simple(const SubstList& discrete_state, } } else if (!options.allVacuity) { - // formula.getRight()->setBypassedDuringProof(true); + formula.getRight()->setBypassedDuringProof(true); } @@ -1752,7 +1755,7 @@ inline void prover::do_proof_place_or_simple(const SubstList& discrete_state, inline void prover::do_proof_place_forall(const SubstList& discrete_state, const DBM& zone, DBMList* place, - const ExprNode& formula) { + ExprNode& formula) { /* Here the model checker looks at the zone of * all time sucessors and then substitutes in * the substitued constraints and sees if the @@ -1808,7 +1811,7 @@ inline void prover::do_proof_place_forall(const SubstList& discrete_state, inline void prover::do_proof_place_forall_rel(const SubstList& discrete_state, const DBM& zone, DBMList* place, - const ExprNode& formula) { + ExprNode& formula) { /* Proof methodology: * first, see if \phi_1 is satisfied during the time advance. * If it is, check that phi_2 is true both at and before those @@ -2015,7 +2018,7 @@ inline void prover::do_proof_place_forall_rel(const SubstList& discrete_state, inline void prover::do_proof_place_exists(const SubstList& discrete_state, const DBM& zone, DBMList* place, - const ExprNode& formula) { + ExprNode& formula) { /* First try to get a new placeholder value that works */ DBM lhs_succ(zone); lhs_succ.suc(); @@ -2068,7 +2071,7 @@ inline void prover::do_proof_place_exists(const SubstList& discrete_state, inline void prover::do_proof_place_exists_rel(const SubstList& discrete_state, const DBM& zone, DBMList* place, - const ExprNode& formula) { + ExprNode& formula) { /* First Try to get a placeholder value that works */ DBM zone_succ(zone); zone_succ.suc(); @@ -2226,7 +2229,7 @@ inline void prover::do_proof_place_exists_rel(const SubstList& discrete_state, inline void prover::do_proof_place_allact(const SubstList& discrete_state, const DBM& zone, DBMList* place, - const ExprNode& formula) { + ExprNode& formula) { /* Enumerate through all transitions */ cpplog(cpplogging::debug) << "\t Proving ALLACT Transitions:----\n" << std::endl; @@ -2345,7 +2348,7 @@ inline void prover::do_proof_place_allact(const SubstList& discrete_state, inline void prover::do_proof_place_existact(const SubstList& discrete_state, const DBM& zone, DBMList* place, - const ExprNode& formula) { + ExprNode& formula) { DBMList result(INFTYDBM); // DBM to accumulate the result. result.makeEmpty(); @@ -2447,7 +2450,7 @@ inline void prover::do_proof_place_existact(const SubstList& discrete_state, inline void prover::do_proof_place_imply(const SubstList& discrete_state, const DBM& zone, DBMList* place, - const ExprNode& formula) { + ExprNode& formula) { DBM zone_copy(zone); /* call comp_ph() for efficient proving of IMPLY's left. */ if (comp_ph(zone_copy, *(formula.getLeft()), discrete_state)) { @@ -2472,7 +2475,7 @@ inline void prover::do_proof_place_imply(const SubstList& discrete_state, inline void prover::do_proof_place_constraint(const DBM& zone, DBMList* place, - const ExprNode& formula) const { + ExprNode& formula) const { if (zone <= *(formula.dbm())) { cpplog(cpplogging::debug) << "---(Valid) Leaf DBM (CONSTRAINT) Reached " "with no need for Placeholder----" @@ -2514,7 +2517,7 @@ inline void prover::do_proof_place_constraint(const DBM& zone, } inline bool prover::do_proof_place_bool(DBMList* place, - const ExprNode& formula) const { + ExprNode& formula) const { bool retVal = (formula.getBool()); cpplog(cpplogging::debug) << "---(" << (retVal ? "V" : "Inv") << "alid) Leaf BOOL Reached----" << std::endl @@ -2529,7 +2532,7 @@ inline bool prover::do_proof_place_bool(DBMList* place, inline bool prover::do_proof_place_atomic(const SubstList& discrete_state, DBMList* place, - const ExprNode& formula) const { + ExprNode& formula) const { bool retVal = (discrete_state.at(formula.getAtomic()) == formula.getIntVal()); cpplog(cpplogging::debug) << "---(" << (retVal ? "V" : "Inv") << "alid) Leaf ATOMIC == Reached----" << std::endl @@ -2543,7 +2546,7 @@ inline bool prover::do_proof_place_atomic(const SubstList& discrete_state, inline bool prover::do_proof_place_atomic_not(const SubstList& discrete_state, DBMList* place, - const ExprNode& formula) const { + ExprNode& formula) const { bool retVal = (discrete_state.at(formula.getAtomic()) != formula.getIntVal()); cpplog(cpplogging::debug) << "---(" << (retVal ? "V" : "Inv") << "alid) Leaf ATOMIC != Reached----" << std::endl @@ -2558,7 +2561,7 @@ inline bool prover::do_proof_place_atomic_not(const SubstList& discrete_state, inline bool prover::do_proof_place_atomic_lt(const SubstList& discrete_state, DBMList* place, - const ExprNode& formula) const { + ExprNode& formula) const { bool retVal = (discrete_state.at(formula.getAtomic()) < formula.getIntVal()); cpplog(cpplogging::debug) << "---(" << (retVal ? "V" : "Inv") << "alid) Leaf ATOMIC < Reached----" << std::endl @@ -2573,7 +2576,7 @@ inline bool prover::do_proof_place_atomic_lt(const SubstList& discrete_state, inline bool prover::do_proof_place_atomic_gt(const SubstList& discrete_state, DBMList* place, - const ExprNode& formula) const { + ExprNode& formula) const { bool retVal = (discrete_state.at(formula.getAtomic()) > formula.getIntVal()); cpplog(cpplogging::debug) << "---(" << (retVal ? "V" : "Inv") << "alid) Leaf ATOMIC > Reached----" << std::endl @@ -2586,7 +2589,7 @@ inline bool prover::do_proof_place_atomic_gt(const SubstList& discrete_state, inline bool prover::do_proof_place_atomic_le(const SubstList& discrete_state, DBMList* place, - const ExprNode& formula) const { + ExprNode& formula) const { bool retVal = (discrete_state.at(formula.getAtomic()) <= formula.getIntVal()); cpplog(cpplogging::debug) << "---(" << (retVal ? "V" : "Inv") << "alid) Leaf ATOMIC < Reached----" << std::endl @@ -2601,7 +2604,7 @@ inline bool prover::do_proof_place_atomic_le(const SubstList& discrete_state, inline bool prover::do_proof_place_atomic_ge(const SubstList& discrete_state, DBMList* place, - const ExprNode& formula) const { + ExprNode& formula) const { bool retVal = (discrete_state.at(formula.getAtomic()) >= formula.getIntVal()); cpplog(cpplogging::debug) << "---(" << (retVal ? "V" : "Inv") << "alid) Leaf ATOMIC > Reached----" << std::endl @@ -2616,7 +2619,7 @@ inline bool prover::do_proof_place_atomic_ge(const SubstList& discrete_state, inline void prover::do_proof_place_sublist(const SubstList& discrete_state, const DBM& zone, DBMList* place, - const ExprNode& formula) { + ExprNode& formula) { SubstList st(formula.getSublist(), &discrete_state); do_proof_place(st, zone, place, *formula.getExpr()); } @@ -2624,7 +2627,7 @@ inline void prover::do_proof_place_sublist(const SubstList& discrete_state, inline void prover::do_proof_place_reset(const SubstList& discrete_state, const DBM& zone, DBMList* place, - const ExprNode& formula) { + ExprNode& formula) { DBM lhs_reset(zone); // JK: It does not become clear why this is necessary here // lhs_reset.bound(input_pes.max_constant()); @@ -2666,7 +2669,7 @@ inline void prover::do_proof_place_reset(const SubstList& discrete_state, inline void prover::do_proof_place_assign(const SubstList& discrete_state, const DBM& zone, DBMList* place, - const ExprNode& formula) { + ExprNode& formula) { DBM lhs_assign(zone); /* Here the DBM zone is where the value of * clock x is reset to clock y, which is possibly @@ -2709,7 +2712,7 @@ inline void prover::do_proof_place_assign(const SubstList& discrete_state, inline void prover::do_proof_place_replace(const SubstList& discrete_state, const DBM& zone, DBMList* place, - const ExprNode& formula) { + ExprNode& formula) { SubstList sub_(discrete_state); sub_[formula.getcX()] = discrete_state.at(formula.getcY()); do_proof_place(sub_, zone, place, *formula.getExpr()); From b7a3d9263741c4aa079e32630df7ab6e28305577 Mon Sep 17 00:00:00 2001 From: Peter Fontana Date: Sun, 2 Feb 2020 21:01:45 -0500 Subject: [PATCH 06/11] Improved Vacuity Checking to include bypassed components. --- pes.timed/ExprNode.cc | 202 +++++++++++++++++++++++++++++++++++++++++- pes.timed/proof.hh | 12 +++ 2 files changed, 213 insertions(+), 1 deletion(-) diff --git a/pes.timed/ExprNode.cc b/pes.timed/ExprNode.cc index 27cc636..d105a46 100644 --- a/pes.timed/ExprNode.cc +++ b/pes.timed/ExprNode.cc @@ -763,5 +763,205 @@ void ExprNode::printExamined(std::ostream& os) if(!(getExaminedDuringProof())) { cout << "*--v--*"; } - + } + +/** Prints out the expression to the desired output stream, labeling + * the expression with its opType. The typical output stream is cout. + * @param e (*) The expression to print out. + * @param os (&) The type of output stream to print the output to. + * param proovVal true if the sequent was proven valid; false otherwise. + * @return None */ +//void ExprNode::printDetectVacuousV1(std::ostream& os, bool proofVal) +//{ +// switch (getOpType()){ +// case PREDICATE: +// os << getPredicate() ; +// break; +// case FORALL: +// os << "FORALL.["; +// getQuant()->printDetectVacuous(os, proofVal); +// os << "]"; +// break; +// case EXISTS: +// os << "EXISTS.["; +// getQuant()->printDetectVacuous(os, proofVal); +// os << "]"; +// break; +// case FORALL_REL: +// os << "FORALLREL.("; +// getLeft()->printDetectVacuous(os, proofVal); +// os << ")["; +// getRight()->printDetectVacuous(os, proofVal); +// os << "]"; +// break; +// case EXISTS_REL: +// os << "EXISTSREL.("; +// getLeft()->printDetectVacuous(os, proofVal); +// os << ")["; +// getRight()->printDetectVacuous(os, proofVal); +// os << "]"; +// break; +// case ALLACT: +// os << "ALLACT.["; +// getQuant()->printDetectVacuous(os, proofVal); +// os << "]"; +// break; +// case EXISTACT: +// os << "EXISTACT.["; +// getQuant()->printDetectVacuous(os, proofVal); +// os << "]"; +// break; +// case AND: +// cout << "("; +// if(proofVal) { +// getLeft()->printDetectVacuous(os, proofVal); +// os << " AND "; +// getRight()->printDetectVacuous(os, proofVal); +// } +// else { +// if(!getRight()->getBypassedDuringProof() && !(getRight()->getValidDuringProof()) ) { +// cout << "*--v--*"; +// } +// getLeft()->printDetectVacuous(os, proofVal); +// if(!getRight()->getBypassedDuringProof() && !(getRight()->getValidDuringProof()) ) { +// cout << "*--v--*"; +// } +// os << " AND "; +// if(!getLeft()->getBypassedDuringProof() && !(getLeft()->getValidDuringProof()) ) { +// cout << "*--v--*"; +// } +// getRight()->printDetectVacuous(os, proofVal); +// if(!getLeft()->getBypassedDuringProof() && !(getLeft()->getValidDuringProof()) ) { +// cout << "*--v--*"; +// } +// } +// cout << ")"; +// break; +// case OR: +// cout << "("; +// if(proofVal) { +// if(!getRight()->getBypassedDuringProof() && !(getRight()->getInvalidDuringProof()) ) { +// cout << "*--v--*"; +// } +// getLeft()->printDetectVacuous(os, proofVal); +// if(!getRight()->getBypassedDuringProof() && !(getRight()->getInvalidDuringProof()) ) { +// cout << "*--v--*"; +// } +// os << " OR "; +// if(!getLeft()->getBypassedDuringProof() && !(getLeft()->getInvalidDuringProof()) ) { +// cout << "*--v--*"; +// } +// getRight()->printDetectVacuous(os, proofVal); +// if(!getLeft()->getBypassedDuringProof() && !(getLeft()->getInvalidDuringProof()) ) { +// cout << "*--v--*"; +// } +// } +// else { +// getLeft()->printDetectVacuous(os, proofVal); +// os << " OR "; +// getRight()->printDetectVacuous(os, proofVal); +// } +// cout << ")"; +// break; +// case OR_SIMPLE: +// cout << "("; +// if(proofVal) { +// if(!getRight()->getBypassedDuringProof() && !(getRight()->getInvalidDuringProof()) ) { +// cout << "*--v--*"; +// } +// getLeft()->printDetectVacuous(os, proofVal); +// if(!getRight()->getBypassedDuringProof() && !(getRight()->getInvalidDuringProof()) ) { +// cout << "*--v--*"; +// } +// os << " OR_S "; +// if(!getLeft()->getBypassedDuringProof() && !(getLeft()->getInvalidDuringProof()) ) { +// cout << "*--v--*"; +// } +// getRight()->printDetectVacuous(os, proofVal); +// if(!getLeft()->getBypassedDuringProof() && !(getLeft()->getInvalidDuringProof()) ) { +// cout << "*--v--*"; +// } +// } +// else { +// getLeft()->printDetectVacuous(os, proofVal); +// os << " OR_S "; +// getRight()->printDetectVacuous(os, proofVal); +// } +// cout << ")"; +// break; +// case IMPLY: +// os << "-(-"; +// getLeft()->printDetectVacuous(os, proofVal); +// os << " IMPLY "; +// getRight()->printDetectVacuous(os, proofVal); +// os << "-)-"; +// break; +// case RESET: +// getExpr()->printDetectVacuous(os, proofVal); +// getClockSet()->print(os); +// break; +// case REPLACE: +// getExpr()->printDetectVacuous(os, proofVal); +// os << "p" << (getAtomic()); +// os << ":="; +// os << getIntVal(); +// break; +// case CONSTRAINT: +// dbm()->print_constraint(os); +// break; +// case ATOMIC: +// os << "p" << (getAtomic()); +// os << "=="; +// os << getIntVal(); +// break; +// case ATOMIC_NOT: +// os << "p" << (getAtomic()); +// os << "!="; +// os << getIntVal(); +// break; +// case ATOMIC_LT: +// os << "p" << (getAtomic()); +// os << "<"; +// os << getIntVal(); +// break; +// case ATOMIC_GT: +// os << "p" << (getAtomic()); +// os << ">"; +// os << getIntVal(); +// break; +// case ATOMIC_LE: +// os << "p" << (getAtomic()); +// os << "<="; +// os << getIntVal(); +// break; +// case ATOMIC_GE: +// os << "p" << (getAtomic()); +// os << ">="; +// os << getIntVal(); +// break; +// case BOOL: +// os << ((getBool())? "TRUE" : "FALSE"); +// break; +// case SUBLIST: +// getExpr()->printDetectVacuous(os, proofVal); +// getSublist()->print(os); +// break; +// case ASSIGN: +// getExpr()->printDetectVacuous(os, proofVal); +// os << "["; +// os << "x" << (getcX()); +// os << "=="; +// os << "x" << (getcY()); +// os << "]"; +// break; +// case ABLEWAITINF: +// os << "AbleWaitInf"; +// break; +// case UNABLEWAITINF: +// os << "UnableWaitInf"; +// break; +// } +// +// +//} diff --git a/pes.timed/proof.hh b/pes.timed/proof.hh index e9b01b8..e760173 100644 --- a/pes.timed/proof.hh +++ b/pes.timed/proof.hh @@ -784,6 +784,9 @@ inline bool prover::do_proof_and(const SubstList& discrete_state, if (retVal) { retVal = do_proof(discrete_state, zone, *formula.getRight()); } + else if(!options.allVacuity){ + formula.getRight()->setBypassedDuringProof(true); + } return retVal; } @@ -813,6 +816,9 @@ inline bool prover::do_proof_or(const SubstList& discrete_state, retVal = do_proof(discrete_state, zone, *formula.getRight()); } else if (placeholder1 >= zone) { retVal = true; + if(!options.allVacuity) { + formula.getRight()->setBypassedDuringProof(true); + } } else { /* Here we get the corner case where we have to use the * OR Split rule, so we try to establish whether part of zone is covered by @@ -840,6 +846,9 @@ inline bool prover::do_proof_or_simple(const SubstList& discrete_state, if (!retVal) { retVal = do_proof(discrete_state, zone, *formula.getRight()); } + else if(!options.allVacuity) { + formula.getRight()->setBypassedDuringProof(true); + } return retVal; } @@ -1672,6 +1681,9 @@ inline void prover::do_proof_place_and(const SubstList& discrete_state, } do_proof_place(discrete_state, zone, place, *formula.getRight()); } + else if(!options.allVacuity){ + formula.getRight()->setBypassedDuringProof(true); + } // delete currPlace; } From ee81cd058887907d072baf171111bce65d08c89e Mon Sep 17 00:00:00 2001 From: Peter Fontana Date: Sun, 5 Apr 2020 15:08:43 -0400 Subject: [PATCH 07/11] Added Vacuity Examples --- .../PFThesisFig6-1aF1.in | 13 +++++++++++++ .../PFThesisFig6-1bF1.in | 13 +++++++++++++ .../AdditionalVacuityCases/PFThesisFig6-2F1.in | 18 ++++++++++++++++++ .../PFThesisFig6-2F1s.in | 18 ++++++++++++++++++ 4 files changed, 62 insertions(+) create mode 100644 examples/AdditionalVacuityCases/PFThesisFig6-1aF1.in create mode 100644 examples/AdditionalVacuityCases/PFThesisFig6-1bF1.in create mode 100644 examples/AdditionalVacuityCases/PFThesisFig6-2F1.in create mode 100644 examples/AdditionalVacuityCases/PFThesisFig6-2F1s.in diff --git a/examples/AdditionalVacuityCases/PFThesisFig6-1aF1.in b/examples/AdditionalVacuityCases/PFThesisFig6-1aF1.in new file mode 100644 index 0000000..56b0fe4 --- /dev/null +++ b/examples/AdditionalVacuityCases/PFThesisFig6-1aF1.in @@ -0,0 +1,13 @@ +CLOCKS :{x1, x2} +CONTROL :{p1(2)} +PREDICATE: {X1, X2} +START: X1 +EQUATIONS: { +1: nu X1 = (p1 != 1 || X2) && (\forall time(X1 && \AllAct(X1))) +2: mu X2 = (p1 == 1) || (\forall time(X2 && \AllAct(X2))) + } +INVARIANT: + p1 == 1 -> x1 <= 50 +TRANSITIONS: + (p1==0, x2 >= 2)->(p1=1){x2}; + (p1==1)->(p1=0){x2}; diff --git a/examples/AdditionalVacuityCases/PFThesisFig6-1bF1.in b/examples/AdditionalVacuityCases/PFThesisFig6-1bF1.in new file mode 100644 index 0000000..1350348 --- /dev/null +++ b/examples/AdditionalVacuityCases/PFThesisFig6-1bF1.in @@ -0,0 +1,13 @@ +CLOCKS :{x1, x2} +CONTROL :{p1(2)} +PREDICATE: {X1, X2} +START: X1 +EQUATIONS: { +1: nu X1 = (p1 != 1 || X2) && (\forall time(X1 && \AllAct(X1))) +2: mu X2 = (p1 == 1) || (\forall time(X2 && \AllAct(X2))) + } +INVARIANT: + p1 == 0 -> x1 >= 0 +TRANSITIONS: + (p1==0)->(p1=0){x1}; + (p1==1)->(p1=0){x2}; diff --git a/examples/AdditionalVacuityCases/PFThesisFig6-2F1.in b/examples/AdditionalVacuityCases/PFThesisFig6-2F1.in new file mode 100644 index 0000000..ffdac38 --- /dev/null +++ b/examples/AdditionalVacuityCases/PFThesisFig6-2F1.in @@ -0,0 +1,18 @@ +CLOCKS :{x1} +CONTROL :{p1(5), p(2), q(2)} +PREDICATE: {X1, X2, X3} +START: X1 +EQUATIONS: { +1: nu X1 = \AllAct(X2 || X3) +2: mu X2 = (p == 1) || (\forall time(X2 && \AllAct(X2))) +3: mu X3 = (q == 1) || (\forall time(X3 && \AllAct(X3))) + } +INVARIANT: + p1 == 0 -> x1 >= 0 +TRANSITIONS: + (p1==0)->(p1=1, p=1, q=0); + (p1==0)->(p1=2, q=1, p=0); + (p1==1)->(p1=3, q=1, p=0); + (p1==3)->(p1=3, q=1, p=0); + (p1==2)->(p1=4, p=1, q=0); + (p1==4)->(p1=4, p=1, q=0); diff --git a/examples/AdditionalVacuityCases/PFThesisFig6-2F1s.in b/examples/AdditionalVacuityCases/PFThesisFig6-2F1s.in new file mode 100644 index 0000000..fba8bb0 --- /dev/null +++ b/examples/AdditionalVacuityCases/PFThesisFig6-2F1s.in @@ -0,0 +1,18 @@ +CLOCKS :{x1} +CONTROL :{p1(5), p(2), q(2)} +PREDICATE: {X1, X2, X3} +START: X1 +EQUATIONS: { +1: nu X1 = \AllAct(X2 |s| X3) +2: mu X2 = (p == 1) |s| \AllAct(X2) +3: mu X3 = (q == 1) |s| \AllAct(X3) + } +INVARIANT: + p1 == 0 -> x1 >= 0 +TRANSITIONS: + (p1==0)->(p1=1, p=1, q=0); + (p1==0)->(p1=2, q=1, p=0); + (p1==1)->(p1=3, q=1, p=0); + (p1==3)->(p1=3, q=1, p=0); + (p1==2)->(p1=4, p=1, q=0); + (p1==4)->(p1=4, p=1, q=0); From 41aae9c8d09b56ee29996c6e7356d245d66ad5ec Mon Sep 17 00:00:00 2001 From: Peter Fontana Date: Sun, 7 Jun 2020 17:24:06 -0400 Subject: [PATCH 08/11] Added Additional Vacuity Examples --- .../PFThesisFig6-2F1sb.in | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) create mode 100644 examples/AdditionalVacuityCases/PFThesisFig6-2F1sb.in diff --git a/examples/AdditionalVacuityCases/PFThesisFig6-2F1sb.in b/examples/AdditionalVacuityCases/PFThesisFig6-2F1sb.in new file mode 100644 index 0000000..26c8a81 --- /dev/null +++ b/examples/AdditionalVacuityCases/PFThesisFig6-2F1sb.in @@ -0,0 +1,17 @@ +CLOCKS :{x1} +CONTROL :{p1(5), p(2), q(2)} +PREDICATE: {X1, X2, X3} +START: X1 +EQUATIONS: { +1: nu X1 = \AllAct(X2) +2: mu X2 = (p == 1) |s| \AllAct(X2) + } +INVARIANT: + p1 == 0 -> x1 >= 0 +TRANSITIONS: + (p1==0)->(p1=1, p=1, q=0); + (p1==0)->(p1=2, q=1, p=0); + (p1==1)->(p1=3, q=1, p=0); + (p1==3)->(p1=3, q=1, p=0); + (p1==2)->(p1=4, p=1, q=0); + (p1==4)->(p1=4, p=1, q=0); From b6cb1ef0e478bb90c1d68e941f50cd0ec9ab9098 Mon Sep 17 00:00:00 2001 From: Peter Fontana Date: Mon, 8 Jun 2020 11:55:48 -0400 Subject: [PATCH 09/11] Cleaned Up Simple Vacuity Implementation --- README.md | 12 +- pes.timed/ExprNode.cc | 417 ------------------------------------- pes.timed/ExprNode.hh | 127 ----------- pes.timed/timesolver-ta.cc | 28 +-- 4 files changed, 16 insertions(+), 568 deletions(-) diff --git a/README.md b/README.md index 91d79dc..1e0837c 100644 --- a/README.md +++ b/README.md @@ -89,7 +89,17 @@ The executable program is named `timesolver-ta`. To run, use `timesolver-ta ` -Example files are included in the `example` directory +Example files are included in the `example` directory. + +### Program Outputs + +The program will output whetehr the formula is vaild or invalid, with the running time. Furthermore, a simple +vacuity is implemented. This program will also identify any unchecked subformulas. This provides a sound +but incomplete vacuity checking for the formula. We know that any subformula not examined during the proof does not +affect the truth of the formula (soundness), however it may check subformula it does not need to check (incompleteness). +The prover checks subformula from left to right. + +To see the entire proof, enable the `-d` option. ## Generating Examples diff --git a/pes.timed/ExprNode.cc b/pes.timed/ExprNode.cc index d105a46..bcbe1a5 100644 --- a/pes.timed/ExprNode.cc +++ b/pes.timed/ExprNode.cc @@ -548,420 +548,3 @@ void ExprNode::printExamined(std::ostream& os) } - -/** Prints out the expression to the desired output stream, labeling - * the expression with its opType. The typical output stream is cout. - * @param e (*) The expression to print out. - * @param os (&) The type of output stream to print the output to. - * param proovVal true if the sequent was proven valid; false otherwise. - * @return None */ - void ExprNode::printDetectVacuous(std::ostream& os, bool proofVal) - { - if(!(getExaminedDuringProof())) { - cout << "*--v--*"; - } - switch (getOpType()){ - case PREDICATE: - os << getPredicate() ; - break; - case FORALL: - os << "FORALL.["; - getQuant()->printDetectVacuous(os, proofVal); - os << "]"; - break; - case EXISTS: - os << "EXISTS.["; - getQuant()->printDetectVacuous(os, proofVal); - os << "]"; - break; - case FORALL_REL: - os << "FORALLREL.("; - getLeft()->printDetectVacuous(os, proofVal); - os << ")["; - getRight()->printDetectVacuous(os, proofVal); - os << "]"; - break; - case EXISTS_REL: - os << "EXISTSREL.("; - getLeft()->printDetectVacuous(os, proofVal); - os << ")["; - getRight()->printDetectVacuous(os, proofVal); - os << "]"; - break; - case ALLACT: - os << "ALLACT.["; - getQuant()->printDetectVacuous(os, proofVal); - os << "]"; - break; - case EXISTACT: - os << "EXISTACT.["; - getQuant()->printDetectVacuous(os, proofVal); - os << "]"; - break; - case AND: - cout << "("; - if(proofVal) { - getLeft()->printDetectVacuous(os, proofVal); - os << " AND "; - getRight()->printDetectVacuous(os, proofVal); - } - else { - if(getLeft()->getExaminedDuringProof() && - !(getRight()->getBypassedDuringProof()) && !(getRight()->getValidDuringProof()) ) { - cout << "*--v--*"; - } - getLeft()->printDetectVacuous(os, proofVal); - if(getLeft()->getExaminedDuringProof() && - !(getRight()->getBypassedDuringProof()) && !(getRight()->getValidDuringProof()) ) { - cout << "*--v--*"; - } - os << " AND "; - if(getRight()->getExaminedDuringProof() && - !(getLeft()->getBypassedDuringProof()) && !(getLeft()->getValidDuringProof()) ) { - cout << "*--v--*"; - } - getRight()->printDetectVacuous(os, proofVal); - if(getRight()->getExaminedDuringProof() && - !(getLeft()->getBypassedDuringProof()) && !(getLeft()->getValidDuringProof()) ) { - cout << "*--v--*"; - } - } - cout << ")"; - break; - case OR: - cout << "("; - if(proofVal) { - if(getLeft()->getExaminedDuringProof() && - !(getRight()->getBypassedDuringProof()) && !(getRight()->getInvalidDuringProof()) ) { - cout << "*--v--*"; - } - getLeft()->printDetectVacuous(os, proofVal); - if(getLeft()->getExaminedDuringProof() && - !(getRight()->getBypassedDuringProof()) && !(getRight()->getInvalidDuringProof()) ) { - cout << "*--v--*"; - } - os << " OR "; - if(getRight()->getExaminedDuringProof() && - !(getLeft()->getBypassedDuringProof()) && !(getLeft()->getInvalidDuringProof()) ) { - cout << "*--v--*"; - } - getRight()->printDetectVacuous(os, proofVal); - if(getRight()->getExaminedDuringProof() && - !(getLeft()->getBypassedDuringProof()) && !(getLeft()->getInvalidDuringProof()) ) { - cout << "*--v--*"; - } - } - else { - getLeft()->printDetectVacuous(os, proofVal); - os << " OR "; - getRight()->printDetectVacuous(os, proofVal); - } - cout << ")"; - break; - case OR_SIMPLE: - cout << "("; - if(proofVal) { - if(getLeft()->getExaminedDuringProof() && - !(getRight()->getBypassedDuringProof()) && !(getRight()->getInvalidDuringProof()) ) { - cout << "*--v--*"; - } - getLeft()->printDetectVacuous(os, proofVal); - if(getLeft()->getExaminedDuringProof() && - !(getRight()->getBypassedDuringProof()) && !(getRight()->getInvalidDuringProof()) ) { - cout << "*--v--*"; - } - os << " OR_S "; - if(getRight()->getExaminedDuringProof() && - !(getLeft()->getBypassedDuringProof()) && !(getLeft()->getInvalidDuringProof()) ) { - cout << "*--v--*"; - } - getRight()->printDetectVacuous(os, proofVal); - if(getRight()->getExaminedDuringProof() && - !(getLeft()->getBypassedDuringProof()) && !(getLeft()->getInvalidDuringProof()) ) { - cout << "*--v--*"; - } - } - else { - getLeft()->printDetectVacuous(os, proofVal); - os << " OR_S "; - getRight()->printDetectVacuous(os, proofVal); - } - cout << ")"; - break; - case IMPLY: - os << "-(-"; - getLeft()->printDetectVacuous(os, proofVal); - os << " IMPLY "; - getRight()->printDetectVacuous(os, proofVal); - os << "-)-"; - break; - case RESET: - getExpr()->printDetectVacuous(os, proofVal); - getClockSet()->print(os); - break; - case REPLACE: - getExpr()->printDetectVacuous(os, proofVal); - os << "p" << (getAtomic()); - os << ":="; - os << getIntVal(); - break; - case CONSTRAINT: - dbm()->print_constraint(os); - break; - case ATOMIC: - os << "p" << (getAtomic()); - os << "=="; - os << getIntVal(); - break; - case ATOMIC_NOT: - os << "p" << (getAtomic()); - os << "!="; - os << getIntVal(); - break; - case ATOMIC_LT: - os << "p" << (getAtomic()); - os << "<"; - os << getIntVal(); - break; - case ATOMIC_GT: - os << "p" << (getAtomic()); - os << ">"; - os << getIntVal(); - break; - case ATOMIC_LE: - os << "p" << (getAtomic()); - os << "<="; - os << getIntVal(); - break; - case ATOMIC_GE: - os << "p" << (getAtomic()); - os << ">="; - os << getIntVal(); - break; - case BOOL: - os << ((getBool())? "TRUE" : "FALSE"); - break; - case SUBLIST: - getExpr()->printDetectVacuous(os, proofVal); - getSublist()->print(os); - break; - case ASSIGN: - getExpr()->printDetectVacuous(os, proofVal); - os << "["; - os << "x" << (getcX()); - os << "=="; - os << "x" << (getcY()); - os << "]"; - break; - case ABLEWAITINF: - os << "AbleWaitInf"; - break; - case UNABLEWAITINF: - os << "UnableWaitInf"; - break; - } - if(!(getExaminedDuringProof())) { - cout << "*--v--*"; - } - - } - -/** Prints out the expression to the desired output stream, labeling - * the expression with its opType. The typical output stream is cout. - * @param e (*) The expression to print out. - * @param os (&) The type of output stream to print the output to. - * param proovVal true if the sequent was proven valid; false otherwise. - * @return None */ -//void ExprNode::printDetectVacuousV1(std::ostream& os, bool proofVal) -//{ -// switch (getOpType()){ -// case PREDICATE: -// os << getPredicate() ; -// break; -// case FORALL: -// os << "FORALL.["; -// getQuant()->printDetectVacuous(os, proofVal); -// os << "]"; -// break; -// case EXISTS: -// os << "EXISTS.["; -// getQuant()->printDetectVacuous(os, proofVal); -// os << "]"; -// break; -// case FORALL_REL: -// os << "FORALLREL.("; -// getLeft()->printDetectVacuous(os, proofVal); -// os << ")["; -// getRight()->printDetectVacuous(os, proofVal); -// os << "]"; -// break; -// case EXISTS_REL: -// os << "EXISTSREL.("; -// getLeft()->printDetectVacuous(os, proofVal); -// os << ")["; -// getRight()->printDetectVacuous(os, proofVal); -// os << "]"; -// break; -// case ALLACT: -// os << "ALLACT.["; -// getQuant()->printDetectVacuous(os, proofVal); -// os << "]"; -// break; -// case EXISTACT: -// os << "EXISTACT.["; -// getQuant()->printDetectVacuous(os, proofVal); -// os << "]"; -// break; -// case AND: -// cout << "("; -// if(proofVal) { -// getLeft()->printDetectVacuous(os, proofVal); -// os << " AND "; -// getRight()->printDetectVacuous(os, proofVal); -// } -// else { -// if(!getRight()->getBypassedDuringProof() && !(getRight()->getValidDuringProof()) ) { -// cout << "*--v--*"; -// } -// getLeft()->printDetectVacuous(os, proofVal); -// if(!getRight()->getBypassedDuringProof() && !(getRight()->getValidDuringProof()) ) { -// cout << "*--v--*"; -// } -// os << " AND "; -// if(!getLeft()->getBypassedDuringProof() && !(getLeft()->getValidDuringProof()) ) { -// cout << "*--v--*"; -// } -// getRight()->printDetectVacuous(os, proofVal); -// if(!getLeft()->getBypassedDuringProof() && !(getLeft()->getValidDuringProof()) ) { -// cout << "*--v--*"; -// } -// } -// cout << ")"; -// break; -// case OR: -// cout << "("; -// if(proofVal) { -// if(!getRight()->getBypassedDuringProof() && !(getRight()->getInvalidDuringProof()) ) { -// cout << "*--v--*"; -// } -// getLeft()->printDetectVacuous(os, proofVal); -// if(!getRight()->getBypassedDuringProof() && !(getRight()->getInvalidDuringProof()) ) { -// cout << "*--v--*"; -// } -// os << " OR "; -// if(!getLeft()->getBypassedDuringProof() && !(getLeft()->getInvalidDuringProof()) ) { -// cout << "*--v--*"; -// } -// getRight()->printDetectVacuous(os, proofVal); -// if(!getLeft()->getBypassedDuringProof() && !(getLeft()->getInvalidDuringProof()) ) { -// cout << "*--v--*"; -// } -// } -// else { -// getLeft()->printDetectVacuous(os, proofVal); -// os << " OR "; -// getRight()->printDetectVacuous(os, proofVal); -// } -// cout << ")"; -// break; -// case OR_SIMPLE: -// cout << "("; -// if(proofVal) { -// if(!getRight()->getBypassedDuringProof() && !(getRight()->getInvalidDuringProof()) ) { -// cout << "*--v--*"; -// } -// getLeft()->printDetectVacuous(os, proofVal); -// if(!getRight()->getBypassedDuringProof() && !(getRight()->getInvalidDuringProof()) ) { -// cout << "*--v--*"; -// } -// os << " OR_S "; -// if(!getLeft()->getBypassedDuringProof() && !(getLeft()->getInvalidDuringProof()) ) { -// cout << "*--v--*"; -// } -// getRight()->printDetectVacuous(os, proofVal); -// if(!getLeft()->getBypassedDuringProof() && !(getLeft()->getInvalidDuringProof()) ) { -// cout << "*--v--*"; -// } -// } -// else { -// getLeft()->printDetectVacuous(os, proofVal); -// os << " OR_S "; -// getRight()->printDetectVacuous(os, proofVal); -// } -// cout << ")"; -// break; -// case IMPLY: -// os << "-(-"; -// getLeft()->printDetectVacuous(os, proofVal); -// os << " IMPLY "; -// getRight()->printDetectVacuous(os, proofVal); -// os << "-)-"; -// break; -// case RESET: -// getExpr()->printDetectVacuous(os, proofVal); -// getClockSet()->print(os); -// break; -// case REPLACE: -// getExpr()->printDetectVacuous(os, proofVal); -// os << "p" << (getAtomic()); -// os << ":="; -// os << getIntVal(); -// break; -// case CONSTRAINT: -// dbm()->print_constraint(os); -// break; -// case ATOMIC: -// os << "p" << (getAtomic()); -// os << "=="; -// os << getIntVal(); -// break; -// case ATOMIC_NOT: -// os << "p" << (getAtomic()); -// os << "!="; -// os << getIntVal(); -// break; -// case ATOMIC_LT: -// os << "p" << (getAtomic()); -// os << "<"; -// os << getIntVal(); -// break; -// case ATOMIC_GT: -// os << "p" << (getAtomic()); -// os << ">"; -// os << getIntVal(); -// break; -// case ATOMIC_LE: -// os << "p" << (getAtomic()); -// os << "<="; -// os << getIntVal(); -// break; -// case ATOMIC_GE: -// os << "p" << (getAtomic()); -// os << ">="; -// os << getIntVal(); -// break; -// case BOOL: -// os << ((getBool())? "TRUE" : "FALSE"); -// break; -// case SUBLIST: -// getExpr()->printDetectVacuous(os, proofVal); -// getSublist()->print(os); -// break; -// case ASSIGN: -// getExpr()->printDetectVacuous(os, proofVal); -// os << "["; -// os << "x" << (getcX()); -// os << "=="; -// os << "x" << (getcY()); -// os << "]"; -// break; -// case ABLEWAITINF: -// os << "AbleWaitInf"; -// break; -// case UNABLEWAITINF: -// os << "UnableWaitInf"; -// break; -// } -// -// -//} diff --git a/pes.timed/ExprNode.hh b/pes.timed/ExprNode.hh index 8a72f37..cc010d1 100644 --- a/pes.timed/ExprNode.hh +++ b/pes.timed/ExprNode.hh @@ -232,10 +232,6 @@ public: bypassedDuringProof = false; validDuringProof = false; invalidDuringProof = false; - validReqDuringProof = false; - invalidReqDuringProof = false; - justRequiredValid = false; - justRequiredInvalid = false; } /** Constructor for two-children expressions with @@ -260,10 +256,6 @@ public: bypassedDuringProof = false; validDuringProof = false; invalidDuringProof = false; - validReqDuringProof = false; - invalidReqDuringProof = false; - justRequiredValid = false; - justRequiredInvalid = false; } /** Constructor for a clock constraint expression with optype = {CONSTRAINT}. @@ -288,10 +280,6 @@ public: bypassedDuringProof = false; validDuringProof = false; invalidDuringProof = false; - validReqDuringProof = false; - invalidReqDuringProof = false; - justRequiredValid = false; - justRequiredInvalid = false; } /** Constructor for a boolean expression of true or false @@ -318,10 +306,6 @@ public: bypassedDuringProof = false; validDuringProof = false; invalidDuringProof = false; - validReqDuringProof = false; - invalidReqDuringProof = false; - justRequiredValid = false; - justRequiredInvalid = false; } /** Constructor for atomic (state value) expressions with @@ -353,10 +337,6 @@ public: bypassedDuringProof = false; validDuringProof = false; invalidDuringProof = false; - validReqDuringProof = false; - invalidReqDuringProof = false; - justRequiredValid = false; - justRequiredInvalid = false; } /** Constructor for invariant sub-expressions with opType = {ATOMIC}. @@ -394,10 +374,6 @@ public: bypassedDuringProof = false; validDuringProof = false; invalidDuringProof = false; - validReqDuringProof = false; - invalidReqDuringProof = false; - justRequiredValid = false; - justRequiredInvalid = false; } /** Constructor for predicate variable expressions with opType = {PREDICATE}. @@ -424,10 +400,6 @@ public: bypassedDuringProof = false; validDuringProof = false; invalidDuringProof = false; - validReqDuringProof = false; - invalidReqDuringProof = false; - justRequiredValid = false; - justRequiredInvalid = false; } /** Constructor for clock set expressions with opType = {RESET}. These @@ -451,10 +423,6 @@ public: bypassedDuringProof = false; validDuringProof = false; invalidDuringProof = false; - validReqDuringProof = false; - invalidReqDuringProof = false; - justRequiredValid = false; - justRequiredInvalid = false; } /** Constructor for sublist expressions, representing a change of @@ -481,10 +449,6 @@ public: bypassedDuringProof = false; validDuringProof = false; invalidDuringProof = false; - validReqDuringProof = false; - invalidReqDuringProof = false; - justRequiredValid = false; - justRequiredInvalid = false; } /** Constructor for assignment and replacement expressions with @@ -520,10 +484,6 @@ public: bypassedDuringProof = false; validDuringProof = false; invalidDuringProof = false; - validReqDuringProof = false; - invalidReqDuringProof = false; - justRequiredValid = false; - justRequiredInvalid = false; } /** Copy Constructor. This is used when an expression needs to be duplicated @@ -604,34 +564,6 @@ public: /* Note: since predicates are shallow-copied, they are not deleted * here. */ } - - /* Note: subformulas are trickier since in circularity */ - void clearValidReq() { - if(validReqDuringProof && justRequiredValid) { - //validReqDuringProof = false; - //justRequiredValid = false; - } - if(left != NULL){ - left->clearValidReq(); - } - if(right != NULL){ - right->clearValidReq(); - } - } - - /* Note: subformulas are trickier since in circularity */ - void clearInvalidReq() { - if(invalidReqDuringProof && justRequiredInvalid) { - //invalidReqDuringProof = false; - //justRequiredInvalid = false; - } - if(left != NULL){ - left->clearInvalidReq(); - } - if(right != NULL){ - right->clearInvalidReq(); - } - } /** Returns the opType of the expression, which labels/categorizes * the expression. @@ -869,33 +801,6 @@ public: return invalidDuringProof; } - /** This returns the value of the boolean - * indicating whether this expression was shown valid by the prover - * and was needed for any left hand sequent. - * @return true: if the expression is valid for some state; - * false: otherwise */ - bool getValidReqDuringProof() { - return validReqDuringProof; - } - - /** This returns the value of the boolean - * indicating whether this expression was shown invalid by the prover - * and was needed for any left hand sequent. - * @return true: if the expression is invalid for some state; - * false: otherwise */ - bool getInvalidReqDuringProof() { - return invalidReqDuringProof; - } - - bool getJustRequiredValid() { - return justRequiredValid; - } - - bool getJustRequiredInvalid() { - return justRequiredInvalid; - } - - /** Records whether this expression was examined by * the PES prover. * @param newVal the boolean value to record. */ @@ -924,28 +829,6 @@ public: invalidDuringProof = newVal; } - /** Records whether this expression was shown valid - * and needed for that branch for some left hand sequent. - * @param newVal the boolean value to record. */ - void setValidReqDuringProof(bool newVal) { - validReqDuringProof = newVal; - } - - /** Records whether this expression was shown invalid - * and needed for that branch for some left hand sequent. - * @param newVal the boolean value to record. */ - void setInvalidReqDuringProof(bool newVal) { - invalidReqDuringProof = newVal; - } - - void setJustRequiredValid(bool newVal) { - justRequiredValid = newVal; - } - - void setJustRequiredInvalid(bool newVal) { - justRequiredInvalid = newVal; - } - protected: /* Note: The data variables here are used as a "quasi-union", * where the same variable can have different uses for different @@ -994,16 +877,6 @@ protected: /** This boolean is true if the PES prover bypassed this subformula * (expression) for some left hand sequent. */ bool bypassedDuringProof; - - /** This boolean is true if the PES prover found this expression - * valid and requierd as valid for any left hand sequent. */ - bool validReqDuringProof; - /** This boolean is true if the PES prover found this expression - * invalid and required invalid for any left hand sequent.*/ - bool invalidReqDuringProof; - - bool justRequiredValid; - bool justRequiredInvalid; /** The "opcode" or Type ID of the Expression Node. * This type determines diff --git a/pes.timed/timesolver-ta.cc b/pes.timed/timesolver-ta.cc index 32a042e..2f7a02d 100644 --- a/pes.timed/timesolver-ta.cc +++ b/pes.timed/timesolver-ta.cc @@ -63,8 +63,8 @@ void printUsage() { std::cerr << "\t option: --version print the version of the tool" << std::endl; std::cerr << "\t option: --no-caching/-n disables performance-optimizing " "known true and known false caches. Circularity stack caching " << "still used." << std::endl; - std::cerr << "\t option: --full-vacuity/-f enables full vacuity checking. " - << " Simple Vacuity is enabled by default" << std::endl; + // std::cerr << "\t option: --full-vacuity/-f enables full vacuity checking. " + // << " Simple Vacuity is enabled by default" << std::endl; } void printVersion() { @@ -121,7 +121,8 @@ void parse_command_line(int argc, char** argv, prover_options& opt) { opt.useCaching = false; break; case 'f': - opt.allVacuity = true; + // Enable once full vacuity checking is implemented + // opt.allVacuity = true; break; case 'v': printVersion(); @@ -308,7 +309,6 @@ int main(int argc, char** argv) { // Print Vacuity output. // First, print which formulas were checked if(!HIDE_VACUITY_OUTPUT){ - std::cout << "Checking with Full Vacuity is " << opt.allVacuity << std::endl; std::cout << "\n====Equation Expressions (**u** expressions unchecked):" << std::endl; for(std::map::const_iterator it = input_pes.equations().begin(); it != input_pes.equations().end(); ++it) { @@ -326,27 +326,9 @@ int main(int argc, char** argv) { } } - // Now print what formulas are vacuous or not - if(!HIDE_VACUITY_OUTPUT) { - std::cout << "\n====Equation Expressions (*--v--* expressions vacuous):" << std::endl; - for(std::map::const_iterator it = input_pes.equations().begin(); - it != input_pes.equations().end(); ++it) { - ExprNode *ls = (*it).second; - - std::cout << (*it).first; - if(ls->get_Parity()) { - std::cout << " :nu= "; - } - else { - std::cout << " :mu= "; - } - ls->printDetectVacuous(std::cout, suc); - std::cout << std::endl; - } - } - cpplog(cpplogging::info) << "==--End of Program Execution-----------------------==" << std::endl; return 0; } + From 20e4cd6660dbe9c8004a8381ea8018c0db515153 Mon Sep 17 00:00:00 2001 From: Peter Fontana Date: Wed, 24 Jun 2020 12:32:10 -0400 Subject: [PATCH 10/11] Reinstated tests --- pes.timed/test/dbmlisttest.cc | 441 ++++++++++++++ pes.timed/test/dbmtest.cc | 1078 +++++++++++++++++++++++++++++++++ pes.timed/test/prooftest.cc | 319 ++++++++++ 3 files changed, 1838 insertions(+) create mode 100644 pes.timed/test/dbmlisttest.cc create mode 100644 pes.timed/test/dbmtest.cc create mode 100644 pes.timed/test/prooftest.cc diff --git a/pes.timed/test/dbmlisttest.cc b/pes.timed/test/dbmlisttest.cc new file mode 100644 index 0000000..d0ec37f --- /dev/null +++ b/pes.timed/test/dbmlisttest.cc @@ -0,0 +1,441 @@ +/** + * Unit tests for DBMList. + * + * + * @author Peter Fontana + * @author Jeroen Keiren + * @copyright MIT Licence, see the accompanying LICENCE.txt. + */ + +#include +#include "DBMList.hh" +#include "testdbms.hh" +#include "gtest/gtest.h" + +/** Use this function only for testing! */ +bool strictly_equal(const DBMList& xs, const DBMList& ys) { + return std::equal(xs.begin(), xs.end(), ys.begin(), [](const DBM& x, const DBM& y) { return x == y; }); +} + +// l1b +DBM testDBM3() +{ + DBM testDBM3(0, 1, bound_to_constraint(-1, weak), make_c2()); + return testDBM3; +} + +// l3a +DBM testDBM4() +{ + DBM testDBM4(make_c2()); + testDBM4.addConstraint(1,0, bound_to_constraint(3, weak)); + testDBM4.addConstraint(2,0, bound_to_constraint(3, weak)); + return testDBM4; +} + +// l3b +DBM testDBM5() +{ + DBM testDBM5(make_c2()); + testDBM5.addConstraint(1,0, bound_to_constraint(4, strict)); + testDBM5.addConstraint(2,0, bound_to_constraint(4, strict)); + testDBM5.addConstraint(0,1, bound_to_constraint(-2, weak)); + testDBM5.addConstraint(0,2, bound_to_constraint(-2, weak)); + return testDBM5; +} + +// l3c +DBM testDBM6() +{ + DBM testDBM6(make_c2()); + testDBM6.addConstraint(2, 1, zero_less); + return testDBM6; +} + +// l4a +DBM testDBM7() +{ + DBM testDBM7(make_c2()); + testDBM7.addConstraint(1,0, bound_to_constraint(1, strict)); + testDBM7.addConstraint(0,1, bound_to_constraint(-2, weak)); + return testDBM7; +} + +// d2a +DBM testDBM8() +{ + DBM testDBM8(make_c2()); + testDBM8.addConstraint(0,1, bound_to_constraint(-1, weak)); + testDBM8.cf(); + return testDBM8; +} + +// d2b +DBM testDBM9() +{ + DBM testDBM9(make_c2()); + testDBM9.addConstraint(1,0, bound_to_constraint(1, strict)); + testDBM9.cf(); + return testDBM9; +} + +// tDBM1 +DBMList testDBMList1() +{ + DBM test1(testDBM1()); + DBMList testDBMList1(test1); + return testDBMList1; +} + +// list1 +DBMList testDBMList3() +{ + DBMList testDBMList3(make_c2()); + DBM test3(testDBM3()); + testDBMList3.addDBM(test3); + return testDBMList3; +} + +// list1b +DBMList testDBMList4() +{ + DBM test3(testDBM3()); + DBMList testDBMList4(test3); + return testDBMList4; +} + +// list3 +DBMList testDBMList5() +{ + DBM test4(testDBM4()); + DBM test5(testDBM5()); + DBM test6(testDBM6()); + DBMList testDBMList5(test4); + testDBMList5.addDBM(test5); + testDBMList5.addDBM(test6); + return testDBMList5; +} + +// list4 +DBMList testDBMList6() +{ + DBM test7(testDBM7()); + DBMList testDBMList6(test7); + return testDBMList6; +} + +// dList2 +DBMList testDBMList7() +{ + DBM test8(testDBM8()); + DBM test9(testDBM9()); + DBMList testDBMList7(test8); + testDBMList7.addDBM(test9); + return testDBMList7; +} + +TEST(DBMListTest, Empty) +{ + DBMList list1cf(testDBMList1()); + DBMList list3cf(testDBMList3()); + DBMList list4cf(testDBMList4()); + DBMList list5cf(testDBMList5()); + list1cf.cf(); + list3cf.cf(); + list4cf.cf(); + list5cf.cf(); + + EXPECT_FALSE(list1cf.emptiness()); + EXPECT_FALSE(list3cf.emptiness()); + EXPECT_FALSE(list4cf.emptiness()); + EXPECT_FALSE(list5cf.emptiness()); +} + +TEST(DBMListTest, CanonicalDBMList1) +{ + DBMList canonical = testDBMList1(); + canonical.cf(); + + DBM test1cf(testDBM1cf()); + DBMList expected(test1cf); + EXPECT_EQ(expected, canonical); +} + +TEST(DBMListTest, CanonicalDBMList3) +{ + DBMList canonical = testDBMList3(); + canonical.cf(); + + DBMList expected(make_c2()); + EXPECT_EQ(expected, canonical); +} + +TEST(DBMListTest, CanonicalDBMList4) +{ + DBMList canonical = testDBMList4(); + canonical.cf(); + + DBMList expected = testDBMList4(); + EXPECT_EQ(expected, canonical); +} + +TEST(DBMListTest, CanonicalDBMList5) +{ + DBMList canonical = testDBMList5(); + canonical.cf(); + + DBM testDBM4cf(make_c2()); + testDBM4cf.addConstraint(0,0, zero_le); + testDBM4cf.addConstraint(0,1, zero_le); + testDBM4cf.addConstraint(0,2, zero_le); + testDBM4cf.addConstraint(1,0, bound_to_constraint(3, weak)); + testDBM4cf.addConstraint(1,1, zero_le); + testDBM4cf.addConstraint(1,2, bound_to_constraint(3, weak)); + testDBM4cf.addConstraint(2,0, bound_to_constraint(3, weak)); + testDBM4cf.addConstraint(2,1, bound_to_constraint(3, weak)); + testDBM4cf.addConstraint(2,2, zero_le); + DBM testDBM5cf(make_c2()); + testDBM5cf.addConstraint(0,0, zero_le); + testDBM5cf.addConstraint(0,1, bound_to_constraint(-2, weak)); + testDBM5cf.addConstraint(0,2, bound_to_constraint(-2, weak)); + testDBM5cf.addConstraint(1,0, bound_to_constraint(4, weak)); + testDBM5cf.addConstraint(1,1, zero_le); + testDBM5cf.addConstraint(1,2, bound_to_constraint(2, weak)); + testDBM5cf.addConstraint(2,0, bound_to_constraint(4, strict)); + testDBM5cf.addConstraint(2,1, bound_to_constraint(2, strict)); + testDBM5cf.addConstraint(2,2, zero_le); + DBM testDBM6cf(make_c2()); + testDBM6cf.addConstraint(0,0, zero_le); + testDBM6cf.addConstraint(0,1, zero_less); + testDBM6cf.addConstraint(0,2, zero_le); + testDBM6cf.addConstraint(1,0, infinity); + testDBM6cf.addConstraint(1,1, zero_le); + testDBM6cf.addConstraint(1,2, infinity); + testDBM6cf.addConstraint(2,0, infinity); + testDBM6cf.addConstraint(2,1, zero_less); + testDBM6cf.addConstraint(2,2, zero_le); + + DBMList expected(testDBM4cf); + expected.addDBM(testDBM5cf); + expected.addDBM(testDBM6cf); + expected.cf(); + + EXPECT_EQ(expected, canonical); +} + +TEST(DBMListTest, CanonicalDBMList6) +{ + DBMList canonical = testDBMList6(); + canonical.cf(); + EXPECT_TRUE(canonical.emptiness()); + + DBM empty(emptyDBM3()); + DBMList expected(empty); + EXPECT_EQ(expected, canonical); + +} + +TEST(DBMListTest, CanonicalDBMList7) +{ + DBMList canonical = testDBMList7(); + canonical.cf(); + + DBMList expected = testDBMList7(); + EXPECT_TRUE(strictly_equal(expected, canonical)); +} + +TEST(DBMListTest, PreDBMList1) +{ + DBMList pre = testDBMList1(); + pre.pre(); + + DBM test1pre(testDBM1pre()); + DBMList expected(test1pre); + EXPECT_EQ(expected, pre); +} + +TEST(DBMListTest, PreCfDBMList1) +{ + DBMList precf = testDBMList1(); + precf.pre(); + precf.cf(); + + DBM test1precf(testDBM1precf()); + DBMList expected(test1precf); + EXPECT_EQ(expected, precf); +} + +TEST(DBMListTest, Subset) +{ + DBMList list3 = testDBMList3(); + DBMList list4 = testDBMList4(); + list3.cf(); + list4.cf(); + DBM infty(make_c2()); + infty.cf(); + + EXPECT_TRUE(list3 <= infty); + EXPECT_TRUE(list4 <= infty); + EXPECT_TRUE(list4 <= list3); + EXPECT_FALSE(list3 <= list4); +} + + +TEST(DBMListTest, Superset) +{ + DBMList list3 = testDBMList3(); + DBMList list4 = testDBMList4(); + list3.cf(); + list4.cf(); + DBM infty(make_c2()); + infty.cf(); + + EXPECT_TRUE(list3 >= infty); + EXPECT_FALSE(list4 >= infty); + EXPECT_FALSE(list4 >= list3); + EXPECT_TRUE(list3 >= list4); +} + +TEST(DBMListTest, Equal) +{ + DBMList list3 = testDBMList3(); + DBMList list4 = testDBMList4(); + DBMList empty = testDBMList3(); + empty.makeEmpty(); + DBM infty(make_c2()); + list3.cf(); + list4.cf(); + + EXPECT_TRUE(list3 == infty); + EXPECT_FALSE(list4 == infty); + EXPECT_FALSE(list4 == list3); + EXPECT_FALSE(list3 == list4); + EXPECT_TRUE(empty == DBMList(emptyDBM3())); + EXPECT_EQ(DBMList(emptyDBM3()), empty); +} + +TEST(DBMListTest, DBMList7Test) +{ + DBMList list7orig = testDBMList7(); + DBMList list7 = testDBMList7(); + DBMList* list7copy = new DBMList(list7); + list7.cf(); + list7copy->cf(); + + EXPECT_EQ(list7, *list7copy); + + list7.cf(); + list7copy->cf(); + EXPECT_FALSE(list7.emptiness()); + EXPECT_FALSE(list7copy->emptiness()); + EXPECT_EQ(list7, (*list7copy)); + EXPECT_TRUE(strictly_equal(list7orig, list7)); + EXPECT_TRUE(strictly_equal(list7orig, *list7copy)); + + DBM infty(make_c2()); + infty.cf(); + EXPECT_TRUE(list7 == infty); + EXPECT_TRUE(strictly_equal(list7, list7orig)); + EXPECT_TRUE(list7 >= infty); + EXPECT_TRUE(strictly_equal(list7, list7orig)); + EXPECT_TRUE(list7 <= infty); + EXPECT_TRUE(strictly_equal(list7, list7orig)); + + delete list7copy; +} + +TEST(DBMListTest, CompareDBMList7Self) +{ + DBMList list7 = testDBMList7(); + list7.cf(); + EXPECT_TRUE(list7 <= list7); + EXPECT_TRUE(list7 >= list7); + EXPECT_TRUE(list7 == list7); +} + +TEST(DBMListTest, CompareDBMList7DBM8) +{ + DBMList list7 = testDBMList7(); + DBM dbm8(testDBM8()); + list7.cf(); + + EXPECT_TRUE(list7 >= dbm8); + EXPECT_FALSE(list7 <= dbm8); + EXPECT_FALSE(list7 == dbm8); +} + +TEST(DBMListTest, Intersection) +{ + DBMList list7orig = testDBMList7(); + DBMList list7 = testDBMList7(); + + list7.intersect(list7orig); + list7.cf(); + DBMList expected = list7orig; + DBM test8(testDBM8()); + DBM test9(testDBM9()); + expected.addDBM(test8); + expected.addDBM(test9); + expected.cf(); + + EXPECT_TRUE(strictly_equal(expected, list7)); + + list7.cf(); + EXPECT_TRUE(strictly_equal(list7orig, list7)); +} + +TEST(DBMListTest, CopyAndIntersectSelf) +{ + DBMList list5 = testDBMList5(); + DBMList list6 = testDBMList6(); + DBMList* list5copy = new DBMList(make_c2()); + *list5copy = list5; + + EXPECT_TRUE(strictly_equal(list5, *list5copy)); + list5.cf(); + list5copy->cf(); + + EXPECT_TRUE(list5 <= *list5copy); + EXPECT_TRUE(list5 >= *list5copy); + EXPECT_TRUE(list5 == *list5copy); + + list5.intersect(*list5copy); + DBMList expected = testDBMList5(); + DBM test4(testDBM4()); + DBM test5(testDBM5()); + DBM test6(testDBM6()); + expected.addDBM(test4); + expected.addDBM(test5); + expected.addDBM(test6); + + list5.cf(); + EXPECT_EQ(*list5copy, list5); + + EXPECT_FALSE(strictly_equal(list5, *list5copy)); + EXPECT_FALSE(strictly_equal(list6, *list5copy)); + + list6.cf(); + EXPECT_TRUE(list5 <= *list5copy); + EXPECT_TRUE(list5 >= *list5copy); + EXPECT_TRUE(list5 == *list5copy); + EXPECT_TRUE(list6 <= *list5copy); + EXPECT_FALSE(list6 >= *list5copy); + EXPECT_FALSE(list6 == *list5copy); + + // test copy + list6 = *list5copy; + EXPECT_TRUE(list6 <= *list5copy); + EXPECT_TRUE(list6 >= *list5copy); + EXPECT_TRUE(list6 == *list5copy); + + list6.cf(); + EXPECT_EQ(list5, list6); + + list6.makeEmpty(); + DBM empty(emptyDBM3()); + DBMList emptylist(empty); + EXPECT_EQ(emptylist, list6); + + delete list5copy; + EXPECT_EQ(emptylist, list6); +} diff --git a/pes.timed/test/dbmtest.cc b/pes.timed/test/dbmtest.cc new file mode 100644 index 0000000..aca13b1 --- /dev/null +++ b/pes.timed/test/dbmtest.cc @@ -0,0 +1,1078 @@ +/** + * Unit tests for DBM. + * + * + * @author Peter Fontana + * @author Jeroen Keiren + * @copyright MIT Licence, see the accompanying LICENCE.txt. + */ + +#include +#include "DBM.hh" +#include "testdbms.hh" +#include "gtest/gtest.h" + +TEST(DBMTest, ClockZero) +{ + clock_value_t zero_strict = zero_less; + EXPECT_EQ(0x0000, zero_strict); + clock_value_t zero_nonstrict = zero_le; + EXPECT_EQ(0x0001, zero_nonstrict); + EXPECT_EQ(zero_strict, bound_to_constraint(0, strict)); + EXPECT_EQ(zero_nonstrict, bound_to_constraint(0, weak)); +} + +TEST(DBMTest, ClockInfty) +{ + clock_value_t infty_strict = infinity; + EXPECT_EQ(infty_strict, std::numeric_limits::max() ^ 1); +} + +TEST(DBMTest, ClockPositive) +{ + clock_value_t one_strict = bound_to_constraint(1, strict); + EXPECT_EQ(0x0002, one_strict); + clock_value_t one_nonstrict = bound_to_constraint(1, weak); + EXPECT_EQ(0x0003, one_nonstrict); + + clock_value_t three_strict = bound_to_constraint(3, strict); + EXPECT_EQ(0x0006, three_strict); + clock_value_t three_nonstrict = bound_to_constraint(3, weak); + EXPECT_EQ(0x0007, three_nonstrict); +} + +TEST(DBMTest, ClockNegative) +{ + clock_value_t neg_one_strict = bound_to_constraint(-1, strict); + EXPECT_EQ(static_cast(0xFFFE), neg_one_strict); // 2's complement repr. of -2 + clock_value_t neg_one_nonstrict = bound_to_constraint(-1, weak); + EXPECT_EQ(static_cast(0xFFFF), neg_one_nonstrict); // 2's complement repr. of -1 + + clock_value_t neg_three_strict = bound_to_constraint(-3, strict); + EXPECT_EQ(static_cast(0xFFFA), neg_three_strict); // 2's complement repr. of -6 + clock_value_t neg_three_nonstrict = bound_to_constraint(-3, weak); + EXPECT_EQ(static_cast(0xFFFB), neg_three_nonstrict); // 2's complement repr. of -5 +} + +DBM testDBM2() +{ + DBM testDBM2(testDBM1()); + testDBM2.addConstraint(2,1, bound_to_constraint(1, weak)); + return testDBM2; +} + +DBM testDBM3() +{ + // Make a third test DBM + DBM testDBM3(make_c2()); + testDBM3.addConstraint(0,0, bound_to_constraint(0, weak)); + testDBM3.addConstraint(0,1, bound_to_constraint(-3, weak)); + testDBM3.addConstraint(0,2, infinity); + testDBM3.addConstraint(1,0, infinity); + testDBM3.addConstraint(1,1, zero_le); + testDBM3.addConstraint(1,2, bound_to_constraint(-5, weak)); + testDBM3.addConstraint(2,0, infinity); + testDBM3.addConstraint(2,1, bound_to_constraint(7, weak)); + testDBM3.addConstraint(2,2, zero_le); + return testDBM3; +} + +DBM testDBM4() +{ + // Make a fourth test DBM - empty + // This is only empty because the (0, <=) becomes (0,<) + // and illustrates a bug in cf() + DBM testDBM4(make_c2()); + testDBM4.addConstraint(0,0, zero_le); + testDBM4.addConstraint(0,1, bound_to_constraint(-3, weak)); + testDBM4.addConstraint(0,2, infinity); + testDBM4.addConstraint(1,0, bound_to_constraint(3, strict)); + testDBM4.addConstraint(1,1, zero_le); + testDBM4.addConstraint(1,2, infinity); + testDBM4.addConstraint(2,0, infinity); + testDBM4.addConstraint(2,1, infinity); + testDBM4.addConstraint(2,2, zero_le); + return testDBM4; +} + +DBM testDBM5() +{ + // Make a fifth test DBM - empty + DBM testDBM5(make_c2()); + testDBM5.addConstraint(0,0, zero_le); + testDBM5.addConstraint(0,1, bound_to_constraint(-4, weak)); + testDBM5.addConstraint(0,2, infinity); + testDBM5.addConstraint(1,0, bound_to_constraint(2, strict)); + testDBM5.addConstraint(1,1, zero_le); + testDBM5.addConstraint(1,2, infinity); + testDBM5.addConstraint(2,0, infinity); + testDBM5.addConstraint(2,1, infinity); + testDBM5.addConstraint(2,2, zero_le); + return testDBM5; +} + +DBM testDBM6() +{ + // Make a sixth test DBM - empty + DBM testDBM6(make_c2()); + testDBM6.addConstraint(0,0, zero_le); + testDBM6.addConstraint(0,1, bound_to_constraint(-1, weak)); + testDBM6.addConstraint(0,2, bound_to_constraint(-1, weak)); + testDBM6.addConstraint(1,0, bound_to_constraint(1, weak)); + testDBM6.addConstraint(1,1, zero_le); + testDBM6.addConstraint(1,2, zero_le); + testDBM6.addConstraint(2,0, bound_to_constraint(2, strict)); + testDBM6.addConstraint(2,1, bound_to_constraint(1, weak)); + testDBM6.addConstraint(2,2, zero_le); + return testDBM6; +} + +DBM testDBM7() +{ + // Make a seventh test DBM - empty + DBM testDBM7(make_c2()); + testDBM7.addConstraint(0,0, zero_le); + testDBM7.addConstraint(0,1, bound_to_constraint(-3, weak)); + testDBM7.addConstraint(0,2, bound_to_constraint(-1, weak)); + testDBM7.addConstraint(1,0, bound_to_constraint(3, weak)); + testDBM7.addConstraint(1,1, zero_le); + testDBM7.addConstraint(1,2, bound_to_constraint(3, weak)); + testDBM7.addConstraint(2,0, bound_to_constraint(6, strict)); + testDBM7.addConstraint(2,1, bound_to_constraint(3, weak)); + testDBM7.addConstraint(2,2, zero_le); + return testDBM7; +} + +DBM testDBM8() +{ + DBM testDBM8(make_c3()); + testDBM8.addConstraint(0,1, bound_to_constraint(-1, weak)); + testDBM8.addConstraint(3,1, bound_to_constraint(6, weak)); + testDBM8.addConstraint(3,2, bound_to_constraint(4, weak)); + return testDBM8; +} + +DBM testDBM9() +{ + DBM testDBM9(make_c3()); + testDBM9.addConstraint(0,1, bound_to_constraint(-1, weak)); + testDBM9.addConstraint(3,2, bound_to_constraint(4, weak)); + return testDBM9; +} + +DBM testDBM10() +{ + DBM testDBM10(make_c3()); + testDBM10.addConstraint(3,1, bound_to_constraint(6, weak)); + testDBM10.addConstraint(3,2, bound_to_constraint(4, weak)); + return testDBM10; +} + +DBM testDBM11() +{ + DBM testDBM11(make_c3()); + testDBM11.addConstraint(2,0,bound_to_constraint(3, weak)); + return testDBM11; +} + +TEST(DBMTest, DefaultIsInfty) +{ + DBM INFTYDBM(make_c2()); + for(size_t i = 0; i <= make_c2()->size();i++) { + for(size_t j = 0; j < make_c2()->size(); j++){ + if(i == j || i == 0){ + INFTYDBM.addConstraint(i,j, zero_le); + } + else { + INFTYDBM.addConstraint(i,j, infinity); + } + } + } + DBM defaultDBM(make_c2()); + EXPECT_EQ(INFTYDBM, defaultDBM); +} + +TEST(DBMTest, Copy) +{ + DBM copy = testDBM1(); + EXPECT_EQ(testDBM1(), copy); +} + +TEST(DBMTest, Emptiness) +{ + EXPECT_TRUE(emptyDBM3().emptiness()); + EXPECT_FALSE(testDBM1().cf().emptiness()); + EXPECT_TRUE(testDBM2().cf().emptiness()); + EXPECT_FALSE(testDBM3().cf().emptiness()); + EXPECT_TRUE(testDBM4().cf().emptiness()); + EXPECT_TRUE(testDBM5().cf().emptiness()); + EXPECT_FALSE(testDBM6().cf().emptiness()); + EXPECT_FALSE(testDBM7().cf().emptiness()); + EXPECT_FALSE(DBM(make_c2()).cf().emptiness()); +} + +TEST(DBMTest, PreEmptyIsEmpty) +{ + DBM preEmpty(emptyDBM3()); + preEmpty.pre(); + preEmpty.cf(); + EXPECT_TRUE(preEmpty.emptiness()); +} + +TEST(DBMTest, CanonicalEmpty) +{ + EXPECT_TRUE(emptyDBM3().cf().emptiness()); + EXPECT_EQ(emptyDBM3(), emptyDBM3().cf()); +} + +TEST(DBMTest, CanonicalDBM1) +{ + DBM canonical(testDBM1()); + canonical.cf(); + EXPECT_FALSE(canonical.emptiness()); + EXPECT_EQ(testDBM1cf(), canonical); +} + +TEST(DBMTest, CanonicalDBM2) +{ + DBM canonical(testDBM2()); + canonical.cf(); + EXPECT_TRUE(canonical.emptiness()); + EXPECT_EQ(emptyDBM3(), canonical); +} + +TEST(DBMTest, CanonicalDBM3) +{ + DBM canonical(testDBM3()); + canonical.cf(); + EXPECT_FALSE(canonical.emptiness()); + + // DBM in canonical form (expected result) + DBM expected(make_c2()); + expected.addConstraint(0,0, zero_le); + expected.addConstraint(0,1, bound_to_constraint(-3, weak)); + expected.addConstraint(0,2, bound_to_constraint(-8, weak)); + expected.addConstraint(1,0, infinity); + expected.addConstraint(1,1, zero_le); + expected.addConstraint(1,2, bound_to_constraint(-5, weak)); + expected.addConstraint(2,0, infinity); + expected.addConstraint(2,1, bound_to_constraint(7, weak)); + expected.addConstraint(2,2, zero_le); + + EXPECT_EQ(expected, canonical); +} + +TEST(DBMTest, CanonicalDBM4) +{ + DBM canonical(testDBM4()); + canonical.cf(); + EXPECT_TRUE(canonical.emptiness()); + EXPECT_EQ(emptyDBM3(), canonical); +} + +TEST(DBMTest, CanonicalDBM5) +{ + DBM canonical(testDBM5()); + canonical.cf(); + EXPECT_TRUE(canonical.emptiness()); + EXPECT_EQ(emptyDBM3(), canonical); +} + +TEST(DBMTest, CanonicalDBM6) +{ + DBM canonical(testDBM6()); + canonical.cf(); + EXPECT_FALSE(canonical.emptiness()); + + // DBM in canonical form (expected result) + DBM expected(make_c2()); + expected.addConstraint(0,0, zero_le); + expected.addConstraint(0,1, bound_to_constraint(-1, weak)); + expected.addConstraint(0,2, bound_to_constraint(-1, weak)); + expected.addConstraint(1,0, bound_to_constraint(1, weak)); + expected.addConstraint(1,1, zero_le); + expected.addConstraint(1,2, zero_le); + expected.addConstraint(2,0, bound_to_constraint(2, strict)); + expected.addConstraint(2,1, bound_to_constraint(1, strict)); + expected.addConstraint(2,2, zero_le); + + EXPECT_EQ(expected, canonical); +} + +TEST(DBMTest, CanonicalDBM7) +{ + DBM canonical(testDBM7()); + canonical.cf(); + EXPECT_FALSE(canonical.emptiness()); + + // DBM in canonical form (expected result) + DBM expected(make_c2()); + expected.addConstraint(0,0, zero_le); + expected.addConstraint(0,1, bound_to_constraint(-3, weak)); + expected.addConstraint(0,2, bound_to_constraint(-1, weak)); + expected.addConstraint(1,0, bound_to_constraint(3, weak)); + expected.addConstraint(1,1, zero_le); + expected.addConstraint(1,2, bound_to_constraint(2, weak)); + expected.addConstraint(2,0, bound_to_constraint(6, strict)); + expected.addConstraint(2,1, bound_to_constraint(3, strict)); + expected.addConstraint(2,2, zero_le); + + EXPECT_EQ(expected, canonical); +} + +TEST(DBMTest, PreDBM1) +{ + DBM pre(testDBM1()); + pre.pre(); + + EXPECT_EQ(testDBM1pre(), pre); +} + +TEST(DBMTest, PreCanonicalDBM1) +{ + DBM pre_cf(testDBM1()); + pre_cf.pre(); + pre_cf.cf(); + + EXPECT_EQ(testDBM1precf(), pre_cf); +} + +TEST(DBMTest, PreCanonicalStrictDBM1) +{ + DBM strict_pred(testDBM1precf()); + strict_pred.predClosureRev(); + + // DBM in canonical form (expected result) + DBM expected(make_c2()); + expected.addConstraint(0,0, zero_le); + expected.addConstraint(0,1, zero_le); + expected.addConstraint(0,2, zero_le); + expected.addConstraint(1,0, bound_to_constraint(3, strict)); + expected.addConstraint(1,1, zero_le); + expected.addConstraint(1,2, bound_to_constraint(3, strict)); + expected.addConstraint(2,0, bound_to_constraint(7, strict)); + expected.addConstraint(2,1, bound_to_constraint(7, strict)); + expected.addConstraint(2,2, zero_le); + + EXPECT_EQ(expected, strict_pred); +} + +TEST(DBMTest, AddDBM1) +{ + DBM add(testDBM1()); + add.addConstraint(0,1, bound_to_constraint(-2, weak)); + + DBM expected(make_c2()); + expected.addConstraint(0,0, zero_le); + expected.addConstraint(0,1, bound_to_constraint(-2, weak)); + expected.addConstraint(0,2, bound_to_constraint(-5, weak)); + expected.addConstraint(1,0, bound_to_constraint(3, weak)); + expected.addConstraint(1,1, zero_le); + expected.addConstraint(1,2, infinity); + expected.addConstraint(2,0, bound_to_constraint(7, weak)); + expected.addConstraint(2,1, infinity); + expected.addConstraint(2,2, zero_le); + + EXPECT_EQ(expected, add); +} + +TEST(DBMTest, AddCanonicalDBM1) +{ + DBM add_canonical(testDBM1()); + add_canonical.addConstraint(0,1, bound_to_constraint(-2, weak)); + add_canonical.cf(); + + DBM expected(make_c2()); + expected.addConstraint(0,0, zero_le); + expected.addConstraint(0,1, bound_to_constraint(-2, weak)); + expected.addConstraint(0,2, bound_to_constraint(-5, weak)); + expected.addConstraint(1,0, bound_to_constraint(3, weak)); + expected.addConstraint(1,1, zero_le); + expected.addConstraint(1,2, bound_to_constraint(-2, weak)); + expected.addConstraint(2,0, bound_to_constraint(7, weak)); + expected.addConstraint(2,1, bound_to_constraint(5, weak)); + expected.addConstraint(2,2, zero_le); + + EXPECT_EQ(expected, add_canonical); +} + +// TODO: The following test is copied from the original, but it should be +// performed on the DBM that has not been changed to canonical form, I think. +TEST(DBMTest, CanonicalBound3DBM2) +{ + DBM bound3(testDBM2()); + bound3.cf(); + bound3.bound(3); + bound3.cf(); + + EXPECT_TRUE(bound3.emptiness()); + EXPECT_EQ(emptyDBM3(), bound3); +} + +TEST(DBMTest, IntersectDBM7DBM6) +{ + DBM left(testDBM7()); + left.cf(); + DBM right(testDBM6()); + right.cf(); + + left.intersect(right); + + DBM expected(make_c2()); + expected.addConstraint(0,0, zero_le); + expected.addConstraint(0,1, bound_to_constraint(-3, weak)); + expected.addConstraint(0,2, bound_to_constraint(-1, weak)); + expected.addConstraint(1,0, bound_to_constraint(1, weak)); + expected.addConstraint(1,1, zero_le); + expected.addConstraint(1,2, zero_le); + expected.addConstraint(2,0, bound_to_constraint(2, strict)); + expected.addConstraint(2,1, bound_to_constraint(1, strict)); + expected.addConstraint(2,2, zero_le); + + EXPECT_EQ(expected, left); + + left.cf(); + EXPECT_TRUE(left.emptiness()); +} + +TEST(DBMTest, IntersectDBM8DBM6) +{ + DBM left(testDBM7()); + left.cf(); + DBM right(testDBM6()); + right.cf(); + + left.intersect(right); + + DBM expected(make_c2()); + expected.addConstraint(0,0, zero_le); + expected.addConstraint(0,1, bound_to_constraint(-3, weak)); + expected.addConstraint(0,2, bound_to_constraint(-1, weak)); + expected.addConstraint(1,0, bound_to_constraint(1, weak)); + expected.addConstraint(1,1, zero_le); + expected.addConstraint(1,2, zero_le); + expected.addConstraint(2,0, bound_to_constraint(2, strict)); + expected.addConstraint(2,1, bound_to_constraint(1, strict)); + expected.addConstraint(2,2, zero_le); + + EXPECT_EQ(expected, left); + left.cf(); + EXPECT_TRUE(left.emptiness()); + EXPECT_EQ(emptyDBM3(), left); +} + +TEST(DBMTest, IntersectDBM8DBM6heap) +{ + DBM* left = new DBM(testDBM7()); + left->cf(); + DBM right(testDBM6()); + right.cf(); + + left->intersect(right); + + DBM expected(make_c2()); + expected.addConstraint(0,0, zero_le); + expected.addConstraint(0,1, bound_to_constraint(-3, weak)); + expected.addConstraint(0,2, bound_to_constraint(-1, weak)); + expected.addConstraint(1,0, bound_to_constraint(1, weak)); + expected.addConstraint(1,1, zero_le); + expected.addConstraint(1,2, zero_le); + expected.addConstraint(2,0, bound_to_constraint(2, strict)); + expected.addConstraint(2,1, bound_to_constraint(1, strict)); + expected.addConstraint(2,2, zero_le); + + EXPECT_EQ(expected, *left); + left->cf(); + EXPECT_TRUE(left->emptiness()); + EXPECT_EQ(emptyDBM3(), *left); +} + +TEST(DBMTest, IntersectDBM8DBM6reference) +{ + DBM temp(testDBM7()); + DBM* left = &temp; + + left->cf(); + DBM right(testDBM6()); + right.cf(); + + left->intersect(right); + + DBM expected(make_c2()); + expected.addConstraint(0,0, zero_le); + expected.addConstraint(0,1, bound_to_constraint(-3, weak)); + expected.addConstraint(0,2, bound_to_constraint(-1, weak)); + expected.addConstraint(1,0, bound_to_constraint(1, weak)); + expected.addConstraint(1,1, zero_le); + expected.addConstraint(1,2, zero_le); + expected.addConstraint(2,0, bound_to_constraint(2, strict)); + expected.addConstraint(2,1, bound_to_constraint(1, strict)); + expected.addConstraint(2,2, zero_le); + + EXPECT_EQ(expected, *left); + left->cf(); + EXPECT_TRUE(left->emptiness()); + EXPECT_EQ(emptyDBM3(), *left); +} + +TEST(DBMTest, ccrepA) +{ + DBM ccrepA(make_c4()); + for (int i=0; i<5; i++) { + ccrepA.addConstraint(i,0, zero_le); + } + + ccrepA.cf(); + EXPECT_FALSE(ccrepA.emptiness()); + + DBM expected(make_c4()); + for (int i=0; i < 5; i++) { + for (int j=0; j < 5; j++) { + expected.addConstraint(i,j, zero_le); + } + } + EXPECT_EQ(expected, ccrepA); + +} + +TEST(DBMTest, empty) +{ + DBM expected(make_c2()); + for (int i=0; i < 3; i++) { + for (int j=0; j < 3; j++) { + expected.addConstraint(i,j, (0x0)); + } + } + EXPECT_EQ(expected, emptyDBM3()); +} + +// Extra tests +TEST(DBMTest, tDBM5) +{ + DBM test(make_c2()); + test.addConstraint(0,2, bound_to_constraint(-3, weak)); + test.addConstraint(1,0, bound_to_constraint(2, weak)); + test.addConstraint(2,0, bound_to_constraint(2, weak)); + + test.cf(); + EXPECT_TRUE(test.emptiness()); + EXPECT_EQ(emptyDBM3(), test); +} + +TEST(DBMTest, Bound1) +{ + /* Make DBM to try to test the correctnes of bound(maxc) */ + DBM test(make_c2()); + test.addConstraint(0,0, zero_le); + test.addConstraint(0,1, bound_to_constraint(-3, weak)); + test.addConstraint(0,2, infinity); + test.addConstraint(1,0, infinity); + test.addConstraint(1,1, zero_le); + test.addConstraint(1,2, infinity); + test.addConstraint(2,0, infinity); + test.addConstraint(2,1, infinity); + test.addConstraint(2,2, zero_le); + + DBM canonical(test); + canonical.cf(); + EXPECT_EQ(test, canonical); + EXPECT_FALSE(canonical.emptiness()); + + test.bound(2); + test.cf(); + EXPECT_FALSE(test.emptiness()); + + DBM expected(make_c2()); + expected.addConstraint(0,0, zero_le); + expected.addConstraint(0,1, bound_to_constraint(-2, strict)); + expected.addConstraint(0,2, infinity); + expected.addConstraint(1,0, infinity); + expected.addConstraint(1,1, zero_le); + expected.addConstraint(1,2, infinity); + expected.addConstraint(2,0, infinity); + expected.addConstraint(2,1, infinity); + expected.addConstraint(2,2, zero_le); + + EXPECT_EQ(expected, test); +} + +TEST(DBMTest, Bound2) +{ + /* Make DBM to try to test the correctnes of bound(maxc) */ + DBM test(make_c2()); + test.addConstraint(0,0, zero_le); + test.addConstraint(0,1, bound_to_constraint(-5, weak)); + test.addConstraint(0,2, infinity); + test.addConstraint(1,0, infinity); + test.addConstraint(1,1, zero_le); + test.addConstraint(1,2, infinity); + test.addConstraint(2,0, infinity); + test.addConstraint(2,1, bound_to_constraint(2, weak)); + test.addConstraint(2,2, zero_le); + + DBM canonical(test); + canonical.cf(); + EXPECT_EQ(test, canonical); + EXPECT_FALSE(canonical.emptiness()); + + test.bound(4); + test.cf(); + EXPECT_FALSE(test.emptiness()); + + DBM expected(make_c2()); + expected.addConstraint(0,0, zero_le); + expected.addConstraint(0,1, bound_to_constraint(-4, strict)); + expected.addConstraint(0,2, infinity); + expected.addConstraint(1,0, infinity); + expected.addConstraint(1,1, zero_le); + expected.addConstraint(1,2, infinity); + expected.addConstraint(2,0, infinity); + expected.addConstraint(2,1, infinity); + expected.addConstraint(2,2, zero_le); + + EXPECT_EQ(expected, test); +} + +TEST(DBMTest, Bound3) +{ + /* Make DBM to try to test the correctnes of bound(maxc) */ + DBM test(make_c2()); + test.addConstraint(0,0, zero_le); + test.addConstraint(0,1, bound_to_constraint(-5, weak)); + test.addConstraint(0,2, infinity); + test.addConstraint(1,0, infinity); + test.addConstraint(1,1, zero_le); + test.addConstraint(1,2, infinity); + test.addConstraint(2,0, bound_to_constraint(1, weak)); + test.addConstraint(2,1, bound_to_constraint(2, weak)); + test.addConstraint(2,2, zero_le); + + // DBM in canonical form, test canonisation works for this instance. + DBM canonical(make_c2()); + canonical.addConstraint(0,0, zero_le); + canonical.addConstraint(0,1, bound_to_constraint(-5, weak)); + canonical.addConstraint(0,2, infinity); + canonical.addConstraint(1,0, infinity); + canonical.addConstraint(1,1, zero_le); + canonical.addConstraint(1,2, infinity); + canonical.addConstraint(2,0, bound_to_constraint(1, weak)); + canonical.addConstraint(2,1, bound_to_constraint(-4, weak)); + canonical.addConstraint(2,2, zero_le); + + test.cf(); + EXPECT_EQ(canonical, test); + EXPECT_FALSE(test.emptiness()); + + // Finally test bounding. + DBM expected(make_c2()); + expected.addConstraint(0,0, zero_le); + expected.addConstraint(0,1, bound_to_constraint(-4, strict)); + expected.addConstraint(0,2, infinity); + expected.addConstraint(1,0, infinity); + expected.addConstraint(1,1, zero_le); + expected.addConstraint(1,2, infinity); + expected.addConstraint(2,0, bound_to_constraint(1, weak)); + expected.addConstraint(2,1, bound_to_constraint(-3, strict)); + expected.addConstraint(2,2, zero_le); + + test.bound(4); + test.cf(); + EXPECT_FALSE(test.emptiness()); + EXPECT_EQ(expected, test); +} + +TEST(DBMTest, Bound4) +{ + /* Make DBM to try to test the correctnes of bound(maxc) */ + DBM test(make_c2()); + test.addConstraint(0,0, zero_le); + test.addConstraint(0,1, bound_to_constraint(-5, weak)); + test.addConstraint(0,2, infinity); + test.addConstraint(1,0, infinity); + test.addConstraint(1,1, zero_le); + test.addConstraint(1,2, infinity); + test.addConstraint(2,0, zero_le); + test.addConstraint(2,1, bound_to_constraint(2, weak)); + test.addConstraint(2,2, zero_le); + + // DBM in canonical form, test canonisation works for this instance. + DBM canonical(make_c2()); + canonical.addConstraint(0,0, zero_le); + canonical.addConstraint(0,1, bound_to_constraint(-5, weak)); + canonical.addConstraint(0,2, infinity); + canonical.addConstraint(1,0, infinity); + canonical.addConstraint(1,1, zero_le); + canonical.addConstraint(1,2, infinity); + canonical.addConstraint(2,0, zero_le); + canonical.addConstraint(2,1, bound_to_constraint(-5, weak)); + canonical.addConstraint(2,2, zero_le); + + test.cf(); + EXPECT_EQ(canonical, test); + EXPECT_FALSE(test.emptiness()); + + // Finally test bounding. + DBM expected(make_c2()); + expected.addConstraint(0,0, zero_le); + expected.addConstraint(0,1, bound_to_constraint(-4, strict)); + expected.addConstraint(0,2, infinity); + expected.addConstraint(1,0, infinity); + expected.addConstraint(1,1, zero_le); + expected.addConstraint(1,2, infinity); + expected.addConstraint(2,0, zero_le); + expected.addConstraint(2,1, bound_to_constraint(-4, strict)); + expected.addConstraint(2,2, zero_le); + + test.bound(4); + test.cf(); + EXPECT_FALSE(test.emptiness()); + EXPECT_EQ(expected, test); +} + +TEST(DBMTest, Bound5) +{ + /* Make DBM to try to test the correctnes of bound(maxc) */ + DBM test(make_c2()); + test.addConstraint(0,0, zero_le); + test.addConstraint(0,1, bound_to_constraint(-5, weak)); + test.addConstraint(0,2, infinity); + test.addConstraint(1,0, infinity); + test.addConstraint(1,1, zero_le); + test.addConstraint(1,2, infinity); + test.addConstraint(2,0, bound_to_constraint(-1, weak)); + test.addConstraint(2,1, bound_to_constraint(2, weak)); + test.addConstraint(2,2, zero_le); + + // DBM in canonical form, test canonisation works for this instance. + DBM canonical(make_c2()); + canonical.addConstraint(0,0, zero_le); + canonical.addConstraint(0,1, bound_to_constraint(-5, weak)); + canonical.addConstraint(0,2, infinity); + canonical.addConstraint(1,0, infinity); + canonical.addConstraint(1,1, zero_le); + canonical.addConstraint(1,2, infinity); + canonical.addConstraint(2,0, bound_to_constraint(-1, weak)); + canonical.addConstraint(2,1, bound_to_constraint(-6, weak)); + canonical.addConstraint(2,2, zero_le); + + test.cf(); + EXPECT_EQ(canonical, test); + EXPECT_FALSE(test.emptiness()); + + // Finally test bounding. + DBM expected(make_c2()); + expected.addConstraint(0,0, zero_le); + expected.addConstraint(0,1, bound_to_constraint(-4, strict)); + expected.addConstraint(0,2, infinity); + expected.addConstraint(1,0, infinity); + expected.addConstraint(1,1, zero_le); + expected.addConstraint(1,2, infinity); + expected.addConstraint(2,0, bound_to_constraint(-1, weak)); + expected.addConstraint(2,1, bound_to_constraint(-4, strict)); + expected.addConstraint(2,2, zero_le); + + test.bound(4); + EXPECT_EQ(expected, test); + test.cf(); + EXPECT_FALSE(test.emptiness()); +} + +TEST(DBMTest, Bound6) +{ + /* Make DBM to try to test the correctnes of bound(maxc) */ + DBM test(make_c2()); + test.addConstraint(0,0, zero_le); + test.addConstraint(0,1, bound_to_constraint(-2, weak)); + test.addConstraint(0,2, infinity); + test.addConstraint(1,0, infinity); + test.addConstraint(1,1, zero_le); + test.addConstraint(1,2, bound_to_constraint(1, strict)); + test.addConstraint(2,0, infinity); + test.addConstraint(2,1, infinity); + test.addConstraint(2,2, zero_le); + + // DBM in canonical form, test canonisation works for this instance. + DBM canonical(make_c2()); + canonical.addConstraint(0,0, zero_le); + canonical.addConstraint(0,1, bound_to_constraint(-2, weak)); + canonical.addConstraint(0,2, bound_to_constraint(-1, strict)); + canonical.addConstraint(1,0, infinity); + canonical.addConstraint(1,1, zero_le); + canonical.addConstraint(1,2, bound_to_constraint(1, strict)); + canonical.addConstraint(2,0, infinity); + canonical.addConstraint(2,1, infinity); + canonical.addConstraint(2,2, zero_le); + + test.cf(); + EXPECT_EQ(canonical, test); + EXPECT_FALSE(test.emptiness()); + + // Finally test bounding. + DBM expected(make_c2()); + expected.addConstraint(0,0, zero_le); + expected.addConstraint(0,1, bound_to_constraint(-1, strict)); + expected.addConstraint(0,2, bound_to_constraint(-1, strict)); + expected.addConstraint(1,0, infinity); + expected.addConstraint(1,1, zero_le); + expected.addConstraint(1,2, bound_to_constraint(1, strict)); + expected.addConstraint(2,0, infinity); + expected.addConstraint(2,1, infinity); + expected.addConstraint(2,2, zero_le); + + test.bound(1); + test.cf(); + EXPECT_FALSE(test.emptiness()); + EXPECT_EQ(expected, test); +} + +TEST(DBMTest, Empty1) +{ + DBM test(make_c2()); + test.addConstraint(0,0, zero_le); + test.addConstraint(0,1, bound_to_constraint(-5, weak)); + test.addConstraint(0,2, infinity); + test.addConstraint(1,0, infinity); + test.addConstraint(1,1, zero_le); + test.addConstraint(1,2, infinity); + test.addConstraint(2,0, infinity); + test.addConstraint(2,1, bound_to_constraint(2, weak)); + test.addConstraint(2,2, zero_le); + + // DBM is already in cf + DBM canonical(test); + canonical.cf(); + EXPECT_EQ(test, canonical); + EXPECT_FALSE(canonical.emptiness()); + + // Normalize + DBM expected(make_c2()); + expected.addConstraint(0,0, zero_le); + expected.addConstraint(0,1, bound_to_constraint(-4, strict)); + expected.addConstraint(0,2, infinity); + expected.addConstraint(1,0, infinity); + expected.addConstraint(1,1, zero_le); + expected.addConstraint(1,2, infinity); + expected.addConstraint(2,0, infinity); + expected.addConstraint(2,1, infinity); + expected.addConstraint(2,2, zero_le); + + test.bound(4); + test.cf(); + EXPECT_EQ(expected, test); + EXPECT_FALSE(test.emptiness()); + + DBM canonical_bound(test); + canonical_bound.cf(); + EXPECT_EQ(test, canonical_bound); +} + +TEST(DBMTest, Empty2) +{ + DBM test(testDBM8()); + + // DBM is already in cf + DBM canonical(test); + canonical.cf(); + EXPECT_EQ(test, canonical); + EXPECT_FALSE(canonical.emptiness()); +} + +TEST(DBMTest, Empty3) +{ + DBM test(testDBM9()); + + // DBM is already in cf + DBM canonical(test); + canonical.cf(); + EXPECT_EQ(test, canonical); + EXPECT_FALSE(canonical.emptiness()); +} + +TEST(DBMTest, Empty4) +{ + DBM test(testDBM10()); + + // DBM is already in cf + DBM canonical(test); + canonical.cf(); + EXPECT_EQ(test, canonical); + EXPECT_FALSE(canonical.emptiness()); +} + +TEST(DBMTest, Empty5) +{ + DBM test(testDBM11()); + + DBM canonical(make_c3()); + canonical.addConstraint(0,0, zero_le); + canonical.addConstraint(0,1, zero_le); + canonical.addConstraint(0,2, zero_le); + canonical.addConstraint(0,3, zero_le); + canonical.addConstraint(1,0, infinity); + canonical.addConstraint(1,1, zero_le); + canonical.addConstraint(1,2, infinity); + canonical.addConstraint(1,3, infinity); + canonical.addConstraint(2,0, bound_to_constraint(3, weak)); + canonical.addConstraint(2,1, bound_to_constraint(3, weak)); + canonical.addConstraint(2,2, zero_le); + canonical.addConstraint(2,3, bound_to_constraint(3, weak)); + canonical.addConstraint(3,0, infinity); + canonical.addConstraint(3,1, infinity); + canonical.addConstraint(3,2, infinity); + canonical.addConstraint(3,3, zero_le); + + test.cf(); + EXPECT_EQ(canonical, test); + EXPECT_FALSE(test.emptiness()); +} + +TEST(DBMTest, IntersectDBM11DBM8) +{ + DBM left(testDBM11()); + left.cf(); + DBM right(testDBM8()); + left.intersect(right); + + DBM expected(make_c3()); + expected.addConstraint(0,0, zero_le); + expected.addConstraint(0,1, bound_to_constraint(-1, weak)); + expected.addConstraint(0,2, zero_le); + expected.addConstraint(0,3, zero_le); + expected.addConstraint(1,0, infinity); + expected.addConstraint(1,1, zero_le); + expected.addConstraint(1,2, infinity); + expected.addConstraint(1,3, infinity); + expected.addConstraint(2,0, bound_to_constraint(3, weak)); + expected.addConstraint(2,1, bound_to_constraint(3, weak)); + expected.addConstraint(2,2, zero_le); + expected.addConstraint(2,3, bound_to_constraint(3, weak)); + expected.addConstraint(3,0, infinity); + expected.addConstraint(3,1, bound_to_constraint(6, weak)); + expected.addConstraint(3,2, bound_to_constraint(4, weak)); + expected.addConstraint(3,3, zero_le); + + EXPECT_EQ(expected, left); + + DBM canonical(make_c3()); + canonical.addConstraint(0,0, zero_le); + canonical.addConstraint(0,1, bound_to_constraint(-1, weak)); + canonical.addConstraint(0,2, zero_le); + canonical.addConstraint(0,3, zero_le); + canonical.addConstraint(1,0, infinity); + canonical.addConstraint(1,1, zero_le); + canonical.addConstraint(1,2, infinity); + canonical.addConstraint(1,3, infinity); + canonical.addConstraint(2,0, bound_to_constraint(3, weak)); + canonical.addConstraint(2,1, bound_to_constraint(2, weak)); + canonical.addConstraint(2,2, zero_le); + canonical.addConstraint(2,3, bound_to_constraint(3, weak)); + canonical.addConstraint(3,0, bound_to_constraint(7, weak)); + canonical.addConstraint(3,1, bound_to_constraint(6, weak)); + canonical.addConstraint(3,2, bound_to_constraint(4, weak)); + canonical.addConstraint(3,3, zero_le); + + left.cf(); + EXPECT_EQ(canonical, left); +} + +TEST(DBMTest, IntersectDBM11DBM9) +{ + DBM left(testDBM11()); + DBM right(testDBM9()); + left.intersect(right); + + DBM expected(make_c3()); + expected.addConstraint(0,0, zero_le); + expected.addConstraint(0,1, bound_to_constraint(-1, weak)); + expected.addConstraint(0,2, zero_le); + expected.addConstraint(0,3, zero_le); + expected.addConstraint(1,0, infinity); + expected.addConstraint(1,1, zero_le); + expected.addConstraint(1,2, infinity); + expected.addConstraint(1,3, infinity); + expected.addConstraint(2,0, bound_to_constraint(3, weak)); + expected.addConstraint(2,1, infinity); + expected.addConstraint(2,2, zero_le); + expected.addConstraint(2,3, infinity); + expected.addConstraint(3,0, infinity); + expected.addConstraint(3,1, infinity); + expected.addConstraint(3,2, bound_to_constraint(4, weak)); + expected.addConstraint(3,3, zero_le); + EXPECT_EQ(expected, left); + + DBM canonical(make_c3()); + canonical.addConstraint(0,0, zero_le); + canonical.addConstraint(0,1, bound_to_constraint(-1, weak)); + canonical.addConstraint(0,2, zero_le); + canonical.addConstraint(0,3, zero_le); + canonical.addConstraint(1,0, infinity); + canonical.addConstraint(1,1, zero_le); + canonical.addConstraint(1,2, infinity); + canonical.addConstraint(1,3, infinity); + canonical.addConstraint(2,0, bound_to_constraint(3, weak)); + canonical.addConstraint(2,1, bound_to_constraint(2, weak)); + canonical.addConstraint(2,2, zero_le); + canonical.addConstraint(2,3, bound_to_constraint(3, weak)); + canonical.addConstraint(3,0, bound_to_constraint(7, weak)); + canonical.addConstraint(3,1, bound_to_constraint(6, weak)); + canonical.addConstraint(3,2, bound_to_constraint(4, weak)); + canonical.addConstraint(3,3, zero_le); + + left.cf(); + EXPECT_EQ(canonical, left); +} + +TEST(DBMTest, IntersectDBM11DBM10) +{ + DBM left(testDBM11()); + DBM right(testDBM10()); + left.intersect(right); + + DBM expected(make_c3()); + expected.addConstraint(0,0, zero_le); + expected.addConstraint(0,1, zero_le); + expected.addConstraint(0,2, zero_le); + expected.addConstraint(0,3, zero_le); + expected.addConstraint(1,0, infinity); + expected.addConstraint(1,1, zero_le); + expected.addConstraint(1,2, infinity); + expected.addConstraint(1,3, infinity); + expected.addConstraint(2,0, bound_to_constraint(3, weak)); + expected.addConstraint(2,1, infinity); + expected.addConstraint(2,2, zero_le); + expected.addConstraint(2,3, infinity); + expected.addConstraint(3,0, infinity); + expected.addConstraint(3,1, bound_to_constraint(6, weak)); + expected.addConstraint(3,2, bound_to_constraint(4, weak)); + expected.addConstraint(3,3, zero_le); + EXPECT_EQ(expected, left); + + DBM canonical(make_c3()); + canonical.addConstraint(0,0, zero_le); + canonical.addConstraint(0,1, zero_le); + canonical.addConstraint(0,2, zero_le); + canonical.addConstraint(0,3, zero_le); + canonical.addConstraint(1,0, infinity); + canonical.addConstraint(1,1, zero_le); + canonical.addConstraint(1,2, infinity); + canonical.addConstraint(1,3, infinity); + canonical.addConstraint(2,0, bound_to_constraint(3, weak)); + canonical.addConstraint(2,1, bound_to_constraint(3, weak)); + canonical.addConstraint(2,2, zero_le); + canonical.addConstraint(2,3, bound_to_constraint(3, weak)); + canonical.addConstraint(3,0, bound_to_constraint(7, weak)); + canonical.addConstraint(3,1, bound_to_constraint(6, weak)); + canonical.addConstraint(3,2, bound_to_constraint(4, weak)); + canonical.addConstraint(3,3, zero_le); + + left.cf(); + EXPECT_EQ(canonical, left); +} + +// Call RUN_ALL_TESTS() in main(). +// +// We do this by linking in src/gtest_main.cc file, which consists of +// a main() function which calls RUN_ALL_TESTS() for us. +// +// This runs all the tests we've defined, prints the result, and +// returns 0 if successful, or 1 otherwise. diff --git a/pes.timed/test/prooftest.cc b/pes.timed/test/prooftest.cc new file mode 100644 index 0000000..fa25c3c --- /dev/null +++ b/pes.timed/test/prooftest.cc @@ -0,0 +1,319 @@ +/** + * Unit tests for prover. + * + * @author Jeroen Keiren + * @copyright MIT Licence, see the accompanying LICENCE.txt. + */ + +#include +#include +#include "proof.hh" +#include "parse.hh" +#include "gtest/gtest.h" + +static +std::string AllActBug( + "CLOCKS: {x}\n" + "CONTROL: {p=1}\n" + "INITIALLY: x == 0\n" + "PREDICATE: {X}\n" + "START: X\n" + "EQUATIONS: {\n" + "1: mu X = \\AllAct(X) && p==1\n" + "}\n" + "INVARIANT:\n" + " p == 1 -> x == 0\n" + "TRANSITIONS:\n" + " (p==1)->(p=2);\n"); + +TEST(ProofTest, AllActBugTest) +{ + pes p; + ASSERT_NO_THROW(parse_pes_from_string(AllActBug, false, p)); + + prover_options options; + prover pr(p, options); + EXPECT_FALSE(pr.do_proof_init(p)); +} + +TEST(ProofTest, AllActBugTestPlace) +{ + pes p; + ASSERT_NO_THROW(parse_pes_from_string(AllActBug, false, p)); + + prover_options options; + prover pr(p, options); + DBMList placeholder(DBM(p.clocks())); + placeholder.cf(); + EXPECT_FALSE(pr.do_proof_init(p, &placeholder)); +} + +static +std::string ExistsBug( + "#define CA 3\n" + "CLOCKS :{x1}\n" + "CONTROL :{p1(1)}\n" + "PREDICATE: {X}\n" + "START: X\n" + "EQUATIONS: {\n" + "1: nu X = (\\exists time(x1 <= 2 && \\forall time(x1 >= 4)))\n" + " }\n"); + +TEST(ProofTest, ExistsBugTest) +{ + pes p; + ASSERT_NO_THROW(parse_pes_from_string(ExistsBug, false, p)); + + prover_options options; + prover pr(p, options); + + EXPECT_FALSE(pr.do_proof_init(p)); + +} + +// In the following example, the property does not hold. However, the placeholder +// that is computed for which the property does hold should be non-empty. +static +std::string ExistsRel( + "CLOCKS: {x1,x2}\n" + "CONTROL: {p1}\n" + "INITIALLY: x1 <= 2 && x2<=1\n" + "PREDICATE: {X}\n" + "START: X\n" + "EQUATIONS: {\n" + "1: mu X = \\exists time\\rel[x1 <= 3](x2==3)\n" + "}\n" + "TRANSITIONS:\n" + ); + +TEST(ProofTest, ExistsRelTestFalse) +{ + pes p; + ASSERT_NO_THROW(parse_pes_from_string(ExistsRel, false, p)); + + prover_options options; + prover pr(p, options); + + DBMList placeholder(DBM(p.clocks())); + placeholder.cf(); + EXPECT_FALSE(pr.do_proof_init(p, &placeholder)); + placeholder.cf(); + + DBM minimum_region(p.clocks()); + minimum_region.addConstraint(1,0, bound_to_constraint(2, weak)); + minimum_region.addConstraint(2,0, bound_to_constraint(1, weak)); + minimum_region.addConstraint(1,2, bound_to_constraint(0, weak)); + + DBM maximum_region1(p.clocks()); + maximum_region1.addConstraint(2,0, bound_to_constraint(3, weak)); + maximum_region1.addConstraint(1,2, bound_to_constraint(0, weak)); + + DBM maximum_region2(p.clocks()); + maximum_region2.addConstraint(2,0, bound_to_constraint(3, weak)); + maximum_region2.addConstraint(2,1, bound_to_constraint(-2, weak)); + + DBMList minimum_placeholder(minimum_region); + minimum_placeholder.cf(); + EXPECT_TRUE(minimum_placeholder <= placeholder); + + DBMList maximum_placeholder(maximum_region1); + maximum_placeholder.addDBM(maximum_region2); + maximum_placeholder.cf(); + EXPECT_TRUE(placeholder <= maximum_placeholder); + + + if(!(minimum_placeholder <= placeholder) || !(placeholder <= maximum_placeholder)) + { + std::cerr << "Resulting placeholder: " << placeholder << std::endl; + std::cerr << "Minimal placeholder: " << minimum_placeholder << std::endl; + std::cerr << "Maximal placeholder: " << maximum_placeholder << std::endl; + } +} + +// In the following example, the initial region is exactly equal to the +// part of the initial region that must be included in the placeholder. +// Therefore, the property must hold. +static +std::string ExistsRelSmallRegion( + "CLOCKS: {x1,x2}\n" + "CONTROL: {p1}\n" + "INITIALLY: x1 <= 2 && x2<=1 && x2 - x1 >= 0\n" + "PREDICATE: {X}\n" + "START: X\n" + "EQUATIONS: {\n" + "1: mu X = \\exists time\\rel[x1 <= 3](x2==3)\n" + "}\n" + "TRANSITIONS:\n" + ); + +TEST(ProofTest, ExistsRelTestTrue) +{ + pes p; + ASSERT_NO_THROW(parse_pes_from_string(ExistsRelSmallRegion, false, p)); + + prover_options options; + prover pr(p, options); + + DBMList placeholder(DBM(p.clocks())); + placeholder.cf(); + EXPECT_TRUE(pr.do_proof_init(p, &placeholder)); + placeholder.cf(); + + DBM minimum_region(p.clocks()); + minimum_region.addConstraint(1,0, bound_to_constraint(2, weak)); + minimum_region.addConstraint(2,0, bound_to_constraint(1, weak)); + minimum_region.addConstraint(1,2, bound_to_constraint(0, weak)); + + DBM maximum_region(p.clocks()); + maximum_region.addConstraint(2,0, bound_to_constraint(3, weak)); + + DBMList minimum_placeholder(minimum_region); + minimum_placeholder.cf(); + EXPECT_TRUE(minimum_placeholder <= placeholder); + + DBMList maximum_placeholder(maximum_region); + maximum_placeholder.cf(); + EXPECT_TRUE(placeholder <= maximum_placeholder); + + + if(!(minimum_placeholder <= placeholder) || !(placeholder <= maximum_placeholder)) + { + std::cerr << "Resulting placeholder: " << placeholder << std::endl; + std::cerr << "Minimal placeholder: " << minimum_placeholder << std::endl; + std::cerr << "Maximal placeholder: " << maximum_placeholder << std::endl; + } +} + +// In the following example, the property holds. The reason for the property +// to hold is that the placeholder for the relativized exists accounts for +// x1 <= 2 && x2 <= 1 && x1 - x2 <= 0; the placeholder for the second disjunct +// accounts for the region x2 - x1 <= 0. Therefore, the entire initial region +// is covered. +static +std::string ExistsRelTrueDueToOr( + "CLOCKS: {x1,x2}\n" + "CONTROL: {p1}\n" + "INITIALLY: x1 <= 2 && x2<=1\n" + "PREDICATE: {X}\n" + "START: X\n" + "EQUATIONS: {\n" + "1: mu X = (\\exists time\\rel[x1 <= 3](x2==3)) || x2 - x1 <= 0\n" + "}\n" + "TRANSITIONS:\n" + ); + +TEST(ProofTest, ExistsRelTestTrueDueToOr) +{ + pes p; + ASSERT_NO_THROW(parse_pes_from_string(ExistsRelTrueDueToOr, false, p)); + + prover_options options; + prover pr(p, options); + + DBMList placeholder(DBM(p.clocks())); + placeholder.cf(); + EXPECT_TRUE(pr.do_proof_init(p, &placeholder)); + placeholder.cf(); +} + +static +std::string RelSplit3( + "CLOCKS: {x1}\n" + "CONTROL: {p1}\n" + "INITIALLY: x1 == 0\n" + "PREDICATE: {X}\n" + "START: X\n" + "EQUATIONS: {\n" + "1: nu X = \\exists time\\rel[x1 <2](x1>=2) || \\forall time(x1 < 2)\n" + "}\n" + "INVARIANT:\n" + " p1 == 0 -> x1 < 3\n" + "TRANSITIONS:\n"); + +TEST(ProofTest, RelSplit3Test) +{ + pes p; + ASSERT_NO_THROW(parse_pes_from_string(RelSplit3, false, p)); + + prover_options options; + prover pr(p, options); + + DBMList placeholder(DBM(p.clocks())); + placeholder.cf(); + EXPECT_TRUE(pr.do_proof_init(p, &placeholder)); + placeholder.cf(); +} + +static +std::string ExistsRelFalseFirstSubformula( + "CLOCKS: {x1}\n" + "CONTROL: {p1}\n" + "INITIALLY: x1 == 0\n" + "PREDICATE: {X}\n" + "START: X\n" + "EQUATIONS: {\n" + "1: nu X = \\exists time\\rel[x1 >= 3](x1 <= 3)\n" + "}\n" + "TRANSITIONS:\n"); + +TEST(ProofTest, ExistsRelFalseFirstSubformulaTest) +{ + pes p; + ASSERT_NO_THROW(parse_pes_from_string(ExistsRelFalseFirstSubformula, false, p)); + + prover_options options; + prover pr(p, options); + + DBMList placeholder(DBM(p.clocks())); + placeholder.cf(); + EXPECT_TRUE(pr.do_proof_init(p, &placeholder)); + placeholder.cf(); +} + +static +std::string TrueCache( + "CLOCKS: {x}\n" + "CONTROL: {p=1}\n" + "INITIALLY: x == 0\n" + "PREDICATE: {X}\n" + "START: X\n" + "EQUATIONS: {\n" + "1: nu X = \\AllAct(X) && p!=1\n" + "}\n" + "INVARIANT:\n" + " p == 1 -> x == 0\n" + "TRANSITIONS:\n" + " (p==1)->(p=1);\n"); + +TEST(ProofTest, TrueCacheTest) +{ + pes p; + ASSERT_NO_THROW(parse_pes_from_string(TrueCache, false, p)); + prover_options options; + prover pr(p, options); + EXPECT_FALSE(pr.do_proof_init(p)); +} + +static +std::string FalseCache( + "CLOCKS: {x}\n" + "CONTROL: {p=1}\n" + "INITIALLY: x == 0\n" + "PREDICATE: {X}\n" + "START: X\n" + "EQUATIONS: {\n" + "1: mu X = \\AllAct(X) || p==1\n" + "}\n" + "INVARIANT:\n" + " p == 1 -> x == 0\n" + "TRANSITIONS:\n" + " (p==1)->(p=1);\n"); + +TEST(ProofTest, FalseCacheTest) +{ + pes p; + ASSERT_NO_THROW(parse_pes_from_string(FalseCache, false, p)); + prover_options options; + prover pr(p, options); + EXPECT_TRUE(pr.do_proof_init(p)); +} From 9cb67fe13a4fb8dbafb94bf23bcbb9c40ba1936c Mon Sep 17 00:00:00 2001 From: Peter Fontana Date: Wed, 24 Jun 2020 12:33:59 -0400 Subject: [PATCH 11/11] reinstated parsetest --- pes.timed/test/parsetest.cc | 58 +++++++++++++++++++++++++++++++++++++ 1 file changed, 58 insertions(+) create mode 100644 pes.timed/test/parsetest.cc diff --git a/pes.timed/test/parsetest.cc b/pes.timed/test/parsetest.cc new file mode 100644 index 0000000..0c49967 --- /dev/null +++ b/pes.timed/test/parsetest.cc @@ -0,0 +1,58 @@ +/** + * Unit tests for Parsing. + * + * @author Jeroen Keiren + * @copyright MIT Licence, see the accompanying LICENCE.txt. + */ + +#include +#include +#include "parse.hh" +#include "gtest/gtest.h" + +#define QUOTE(name) #name +#define STR(macro) QUOTE(macro) +#define EXAMPLES_DIR_NAME STR(EXAMPLES_DIR) + +std::string AFSpecA1String( + "CLOCKS :{x1}\n" + "CONTROL :{p1(2)}\n" + "PREDICATE: {X1}\n" + "START: X1\n" + "EQUATIONS: {\n" + "1: mu X1 = p1 == 1\n" + " || ((\\forall time( \n" + "( (p1 == 0) -> (X1[p1=0][x1]))\n" + "&& ( (p1 == 0) -> (X1[p1=1]))\n" + "&& ( (p1 == 1) -> (X1[p1=1])))))\n" + "}\n" + "INVARIANT:\n" + " p1 == 0 -> x1 <= 2\n"); + +TEST(ParseTest, ParseFile) +{ + pes p; + std::string filename(std::string(EXAMPLES_DIR_NAME) + "/CorrectnessTestSuite/Invalid/Liveness/AFSpecA1.in"); + ASSERT_NO_THROW(parse_pes(filename, false, p)); + + EXPECT_EQ(1, p.clocks()->size()); + EXPECT_EQ(1, p.atomic()->size()); + EXPECT_EQ("X1", p.start_predicate()); +} + +TEST(ParseTest, ParseNonexistantFile) +{ + pes p; + std::string filename(std::string(EXAMPLES_DIR_NAME) + "/Nonexistant.in"); + EXPECT_ANY_THROW(parse_pes(filename, false, p)); +} + +TEST(ParseTest, ParseString) +{ + pes p; + ASSERT_NO_THROW(parse_pes_from_string(AFSpecA1String, false, p)); + + EXPECT_EQ(1, p.clocks()->size()); + EXPECT_EQ(1, p.atomic()->size()); + EXPECT_EQ("X1", p.start_predicate()); +}