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 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/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); 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); 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..bcbe1a5 100644 --- a/pes.timed/ExprNode.cc +++ b/pes.timed/ExprNode.cc @@ -397,3 +397,154 @@ 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**"; + } + + +} diff --git a/pes.timed/ExprNode.hh b/pes.timed/ExprNode.hh index ee8247a..cc010d1 100644 --- a/pes.timed/ExprNode.hh +++ b/pes.timed/ExprNode.hh @@ -228,6 +228,10 @@ public: predicate = nullptr; subst = nullptr; assert(q != nullptr); + examinedDuringProof = false; + bypassedDuringProof = false; + validDuringProof = false; + invalidDuringProof = false; } /** Constructor for two-children expressions with @@ -248,6 +252,10 @@ public: subst = nullptr; assert(l != nullptr); assert(r != nullptr); + examinedDuringProof = false; + bypassedDuringProof = false; + validDuringProof = false; + invalidDuringProof = false; } /** Constructor for a clock constraint expression with optype = {CONSTRAINT}. @@ -268,6 +276,10 @@ public: constraint = c; m_clock_set = nullptr; subst = nullptr; + examinedDuringProof = false; + bypassedDuringProof = false; + validDuringProof = false; + invalidDuringProof = false; } /** Constructor for a boolean expression of true or false @@ -290,6 +302,10 @@ public: constraint = nullptr; m_clock_set = nullptr; subst = nullptr; + examinedDuringProof = false; + bypassedDuringProof = false; + validDuringProof = false; + invalidDuringProof = false; } /** Constructor for atomic (state value) expressions with @@ -317,6 +333,10 @@ public: subst = nullptr; m_clock_set = nullptr; constraint = nullptr; + examinedDuringProof = false; + bypassedDuringProof = false; + validDuringProof = false; + invalidDuringProof = false; } /** Constructor for invariant sub-expressions with opType = {ATOMIC}. @@ -350,6 +370,10 @@ public: predicate = nullptr; m_clock_set = nullptr; subst = nullptr; + examinedDuringProof = false; + bypassedDuringProof = false; + validDuringProof = false; + invalidDuringProof = false; } /** Constructor for predicate variable expressions with opType = {PREDICATE}. @@ -372,6 +396,10 @@ public: m_clock_set = nullptr; subst = nullptr; constraint = nullptr; + examinedDuringProof = false; + bypassedDuringProof = false; + validDuringProof = false; + invalidDuringProof = false; } /** Constructor for clock set expressions with opType = {RESET}. These @@ -391,6 +419,10 @@ public: predicate = nullptr; constraint = nullptr; subst = nullptr; + examinedDuringProof = false; + bypassedDuringProof = false; + validDuringProof = false; + invalidDuringProof = false; } /** Constructor for sublist expressions, representing a change of @@ -413,6 +445,10 @@ public: predicate = nullptr; m_clock_set = nullptr; constraint = nullptr; + examinedDuringProof = false; + bypassedDuringProof = false; + validDuringProof = false; + invalidDuringProof = false; } /** Constructor for assignment and replacement expressions with @@ -444,6 +480,10 @@ public: m_clock_set = nullptr; constraint = nullptr; subst = nullptr; + examinedDuringProof = false; + bypassedDuringProof = false; + validDuringProof = false; + invalidDuringProof = false; } /** Copy Constructor. This is used when an expression needs to be duplicated @@ -539,16 +579,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 +681,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,7 +768,67 @@ 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; + } + + /** 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; + } + protected: /* Note: The data variables here are used as a "quasi-union", * where the same variable can have different uses for different @@ -753,6 +862,21 @@ 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; /** The "opcode" or Type ID of the Expression Node. * This type determines @@ -798,6 +922,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..e760173 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.setValidDuringProof(true); + } + else { + formula.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,113 @@ protected: break; } } + if(!options.allVacuity) { + if(place!=NULL) { + place->cf(); + if(!(place->emptiness())) { + formula.setValidDuringProof(true); + } + } + else { + formula.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 +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 */ @@ -723,7 +750,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,13 +777,16 @@ 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()); if (retVal) { retVal = do_proof(discrete_state, zone, *formula.getRight()); } + else if(!options.allVacuity){ + formula.getRight()->setBypassedDuringProof(true); + } return retVal; } @@ -767,7 +797,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 */ @@ -786,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 @@ -807,18 +840,21 @@ 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) { retVal = do_proof(discrete_state, zone, *formula.getRight()); } + else if(!options.allVacuity) { + formula.getRight()->setBypassedDuringProof(true); + } return retVal; } // [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 +876,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 +1052,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 +1104,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 +1287,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 +1382,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 +1490,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 +1518,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 +1528,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 +1542,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 +1551,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 +1560,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,23 +1669,33 @@ 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()); } + else if(!options.allVacuity){ + formula.getRight()->setBypassedDuringProof(true); + } + // 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()); 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 @@ -1667,6 +1713,7 @@ inline void prover::do_proof_place_or(const SubstList& discrete_state, << "\nRight Placeholder of OR (P): " << *place << std::endl; } + place->union_(placeholder_left); place->cf(); @@ -1674,12 +1721,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, - 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 +1756,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 +1767,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 +1823,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 +2030,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 +2083,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 +2241,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 +2360,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 +2462,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 +2487,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 +2529,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 +2544,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 +2558,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 +2573,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 +2588,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 +2601,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 +2616,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 +2631,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 +2639,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 +2681,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 +2724,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 2c24cfa..80d3d1a 100644 --- a/pes.timed/prover_options.hh +++ b/pes.timed/prover_options.hh @@ -23,6 +23,10 @@ struct prover_options { /** If True, use tables in the output. Else (False), * print regular output. */ bool tabled; + + /* If True, enable full vacuity. Else, run + * with simple vacuity. */ + bool allVacuity; /** The size of the Hash table of Sequents: nBits + 1 */ unsigned long nHash; diff --git a/pes.timed/timesolver-ta.cc b/pes.timed/timesolver-ta.cc index 7b817e0..2f7a02d 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 @@ -61,9 +62,9 @@ void printUsage() { std::cerr << "\t option: --help/-h this help info" << std::endl; 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; + "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; } void printVersion() { @@ -73,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 = "dDhntH:"; + const char* const short_opts = "dDhntHf:"; const option long_opts[] { {"debug", 0, nullptr, 'd'}, {"full-debug", 0, nullptr, 'D'}, @@ -82,6 +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'}, + {"allVacuity", 0, nullptr, 'f'}, {nullptr, 0, nullptr, 0} }; @@ -118,6 +120,10 @@ void parse_command_line(int argc, char** argv, prover_options& opt) { case 'n': opt.useCaching = false; break; + case 'f': + // Enable once full vacuity checking is implemented + // opt.allVacuity = true; + break; case 'v': printVersion(); exit(1); @@ -299,9 +305,30 @@ 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 << "\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; + } + } + cpplog(cpplogging::info) << "==--End of Program Execution-----------------------==" << std::endl; return 0; } + 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