Merge branch 'carlo-dev_OU' into OU-master

Author: carlosengers

.idea/.name

@@ -1,4 +1,6 @@
-cmake_minimum_required(VERSION 3.14)
+# this makefile is intended to be used  on a full Ubuntu 18.04 VM and CLION IDE.
+# with SPOT pre-installed.
+cmake_minimum_required(VERSION 3.10)
 project(spot_checker)
 
 set(CMAKE_CXX_STANDARD 17)
@@ -8,7 +10,10 @@ set(CMAKE_CXX_STANDARD 17)
 include_directories(/home/css/spot-2.7.2)   # for spot header files. when installed via config+make
 include_directories(/home/css/usr/include)   #for bddx.h file
 link_directories(/home/css/usr/lib)
-add_executable(spot_checker spot_checker.cpp)
-target_link_libraries(spot_checker libspot.so libbddx.so libstdc++fs.a) #libstdc++fs.a for filesystem exeprimental
 
+add_executable(spot_checker spot_checker.cpp )
+target_link_libraries(spot_checker  libspot.so libbddx.so libstdc++fs.a) #libstdc++fs.a for filesystem exeprimental
+
+#add_executable(spot_formula_to_dot spot_formula_to_dot.cpp)
+#target_link_libraries( spot_formula_to_dot libspot.so libbddx.so libstdc++fs.a) #libstdc++fs.a for filesystem exeprimental
 

CMakeLists.txt

@@ -0,0 +1,16 @@
+# still experimental: this makefile is intended to be used  on a Win10 machine with CLION IDE and Ubuntu 18.04 WSL configured.
+# with SPOT pre-installed on the WSL distro.
+cmake_minimum_required(VERSION 3.14)
+project(spot_checker)
+set(CMAKE_SYSTEM_NAME Linux)
+set(CMAKE_CXX_STANDARD 17)
+#set(CMAKE_MODULE_PATH "/home/css/usr/lib/;${CMAKE_MODULE_PATH}")
+#set (CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -std=c++1y -O2 -std=c++11 -I/usr/local/include -L/usr/local/lib -lboost_system -lboost_filesystem -fopenmp -lpthread -lz")
+#set (CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -lstdc++fs -std=c++17")
+include_directories(C:\spot-2.8.7\spot)   # for spot header files. when installed via config+make
+include_directories(C:\spot-2.8.7\buddy\src)   #for bddx.h file
+link_directories(C:\spot-2.8.7\lib)
+add_executable(spot_checker spot_checker.cpp)
+target_link_libraries(spot_checker libspot.so libbddx.so libstdc++fs.a) #libstdc++fs.a for filesystem exeprimental
+
+

CMakeListsCross.txt

@@ -1,75 +1,47 @@
-# spot_checker
 
-
-- This utility program is a wrapper around SPOT for usage with TESTAR.
-  - The code of the model checker is from the SPOT library (https://spot.lrde.epita.fr/).
-  - The wrapper takes in a file with an automaton and (a file with) formulas
-  - and returns the results in a format that TESTAR is able to parse.
-  - The command is developed on  Ubuntu 18.04 and is intended to run on Windows Subsystem for Linux (WSL).
-  - WSL v1903 or higher is recommended.
+# spot\_checker
+This utility program is a wrapper around SPOT library (https://spot.lrde.epita.fr/) for usage with TESTAR.  
+The main purpose is to convert LTL formulas to finite LTL (LTLF) variants before they are model checked.  
+LTLF can be use full for models with terminal states.
+
+The application weaves an atomic proposition (AP) into the formula to label the 'alive' part of the model.  E.g. '\--ltlf !dead or \--ltlf alive'.  
+The wrapper takes in a file with an automaton and (a file with) formulas and returns the results in a format that TESTAR is able to parse.  
+The command is developed on  Ubuntu 18.04 and is intended to run on Windows Subsystem for Linux (WSL). WSL v1903 or higher is recommended  
+
+Note: 
+- This 'terminal' AP MUST exist in the automaton as well!!  
+- Terminal states in the model shall have a self-loop with 'dead' or '!alive'  as the only property that holds
+- or Terminal states always transition to an artificial terminal state with such a self-loop. 
+ 
+LTLF variant | use case
+------------ | -------- 
+LTLf (G&V-2013) | for plain traces or a DAG.  
+LTLfs           | for safety properties on models with terminal states.  
+LTLfl           | for liveness properties* on models with terminal states. 
+ *<i>Checked in non-trivial SCC's only and <u>NOT</u> in the finite suffix towards a terminal
+  state</i>
 
-
-Program version : 20200823
+Program version : 20201024
 
 ---
 #### Usage:  
-spot_checker &nbsp;&nbsp; \--stdin --a *file* \--sf *formula* \--ff *file* \--fonly  --ltlf  *str* \--ltlxf *str* \--witness  *file*
-Help is displyed when the spot_checker is invoked without options.
+spot_checker &nbsp;&nbsp; \--stdin --a *file* \--sf *formula* \--ff *file* \--fonly  --ltlf  *str* \--ltlxf *str* \--witness    
+Help is displayed when the spot_checker is invoked without options.
+All output is send to stdout.
 
 #### Commandline options:
-
-##### \--stdin   
-optional.  
-*  all input is  via standard input stream: 
-*  at first an automaton  [HOA format](http://adl.github.io/hoaf/) . 'EOF_HOA' + newline  marks the end of the automaton.
-*  followed by formulas.
-*  all other arguments are ignored and output is via stdout.
-
-##### \--a       
-mandatory.  
-unless --stdin is the argument. filename containing the automaton (HOA format). 
-
-
-##### \--sf      
-optional.  
-the single LTL formula/property to check.  
-
-
-##### \--ff      
-optional.  
-filename containing multiple formulas/properties. 
-
-
-##### \--fonly       
-optional.  
-Does not check against a model, but only verifies the formulas --sf or --ff syntactically and provides LTLF versions.    
-    (the alive property is taken from --ltlf or --ltlxf and by absence the program  uses '!dead').  
-    This option ignores --a, --witness.
-
-##### \--ltlf    
-optional.  
-usable for finite LTL (if the automaton contains terminal states):
-Weaves an atomic proposition(AP) into the formula to label the 'alive' part. E.g. '--ltlf !dead or --ltlf alive'.
-Note: this AP MUST exist in the automaton as well!! 
-Terminal states in the model shall have a self-loop with 'dead' or '!alive' 
-as the only property or always transition to an artificial terminal state with such a self-loop. Variants:  
-          LTLf (G&V-2013) : for traces or a DAG.  
-          LTLfs           : for safety properties on models with terminal states.  
-          LTLfl           : for liveness properties (in SCC's) on models with terminal states.  
-
-##### \--ltlxf   
-optional.  
-checks **both** the original formula and **all** the ltlf variants
-
-##### \--witness 
-optional.  
-generates a trace: counterexample (for FAIL) or witness (for PASS)
+Option   | mandatory | Usage
+-------- | --------- | -----
+\--stdin | optional  | All input is  via console:  <br> first a single automaton in [HOA format](http://adl.github.io/hoaf/) (http://adl.github.io/hoaf/) followed by formulas. <br> When completed, the system will ask for a new formula to model check. <br>A blank line will stop the program and all other arguments are ignored.
+\--a     | mandatory unless <br>\--stdin is used |  filename containing the automaton (HOA format) <br> Without \--sf or \--ff, the formula/property is via stdin. 
+\--sf    | optional  | the single LTL formula/property to check. Add quotes if the formula contains spaces
+\--ff    | optional  | filename containing multiple formulas/properties. 
+\--fonly | optional  | Does not check against a model, but only verifies the formulas  syntactically and provides LTLF versions. <br>The alive property to be  provided by \--ltlf or \--ltlxf. By absence the program  uses '!dead'. This option ignores \--a, \--witness.
+\--ltlf  | optional  | the alive property: E.g.  '!dead' or 'alive'. 
+\--ltlx  | optional  | without \--fonly: model check both the original formula and all the ltlf variants
+\--witness| optional  | generates a trace: counterexample (for FAIL) or witness (for PASS)
 
 ---
-#### Use-case when only option --a is supplied (without --sf or --ff): 
-
-          The user can supply via stdin a formula/property. Results are returned via stdout.
-          The system will ask for a new formula. A blank line will stop the program. 
 
 #### Note:     
 

README.md

@@ -1,4 +1,4 @@
-# Doxyfile 1.8.17
+# Doxyfile 1.8.20
 
 # This file describes the settings to be used by the documentation system
 # doxygen (www.doxygen.org) for a project.
@@ -38,7 +38,7 @@ PROJECT_NAME           = "Testar Wrapper for SPOT Modelchecker"
 # could be handy for archiving the generated documentation or if some version
 # control system is used.
 
-PROJECT_NUMBER         = v0.82
+PROJECT_NUMBER         = v0.87
 
 # Using the PROJECT_BRIEF tag one can provide an optional one line description
 # for a project that appears at the top of each page and should give viewer a
@@ -58,7 +58,7 @@ PROJECT_LOGO           = C:/Users/cseng/git/testar_LTL/doxygen/testar_logo.png
 # entered, it will be relative to the location where doxygen was started. If
 # left blank the current directory will be used.
 
-OUTPUT_DIRECTORY       = .
+OUTPUT_DIRECTORY       =
 
 # If the CREATE_SUBDIRS tag is set to YES then doxygen will create 4096 sub-
 # directories (in 2 levels) under the output directory of each output format and
@@ -227,6 +227,14 @@ QT_AUTOBRIEF           = NO
 
 MULTILINE_CPP_IS_BRIEF = NO
 
+# By default Python docstrings are displayed as preformatted text and doxygen's
+# special commands cannot be used. By setting PYTHON_DOCSTRING to NO the
+# doxygen's special commands can be used and the contents of the docstring
+# documentation blocks is shown as doxygen documentation.
+# The default value is: YES.
+
+PYTHON_DOCSTRING       = YES
+
 # If the INHERIT_DOCS tag is set to YES then an undocumented member inherits the
 # documentation from any documented member that it re-implements.
 # The default value is: YES.
@@ -263,12 +271,6 @@ TAB_SIZE               = 4
 
 ALIASES                =
 
-# This tag can be used to specify a number of word-keyword mappings (TCL only).
-# A mapping has the form "name=value". For example adding "class=itcl::class"
-# will allow you to use the command class in the itcl::class meaning.
-
-TCL_SUBST              =
-
 # Set the OPTIMIZE_OUTPUT_FOR_C tag to YES if your project consists of C sources
 # only. Doxygen will then generate output that is more tailored for C. For
 # instance, some of the names that are used will be different. The list of all
@@ -310,13 +312,13 @@ OPTIMIZE_OUTPUT_SLICE  = NO
 # extension. Doxygen has a built-in mapping, but you can override or extend it
 # using this tag. The format is ext=language, where ext is a file extension, and
 # language is one of the parsers supported by doxygen: IDL, Java, JavaScript,
-# Csharp (C#), C, C++, D, PHP, md (Markdown), Objective-C, Python, Slice,
+# Csharp (C#), C, C++, D, PHP, md (Markdown), Objective-C, Python, Slice, VHDL,
 # Fortran (fixed format Fortran: FortranFixed, free formatted Fortran:
 # FortranFree, unknown formatted Fortran: Fortran. In the later case the parser
 # tries to guess whether the code is fixed or free formatted code, this is the
-# default for Fortran type files), VHDL, tcl. For instance to make doxygen treat
-# .inc files as Fortran files (default is PHP), and .f files as C (default is
-# Fortran), use: inc=Fortran f=C.
+# default for Fortran type files). For instance to make doxygen treat .inc files
+# as Fortran files (default is PHP), and .f files as C (default is Fortran),
+# use: inc=Fortran f=C.
 #
 # Note: For files without extension you can use no_extension as a placeholder.
 #
@@ -366,7 +368,7 @@ BUILTIN_STL_SUPPORT    = NO
 # enable parsing support.
 # The default value is: NO.
 
-CPP_CLI_SUPPORT        = YES
+CPP_CLI_SUPPORT        = NO
 
 # Set the SIP_SUPPORT tag to YES if your project consists of sip (see:
 # https://www.riverbankcomputing.com/software/sip/intro) sources only. Doxygen
@@ -455,6 +457,19 @@ TYPEDEF_HIDES_STRUCT   = NO
 
 LOOKUP_CACHE_SIZE      = 0
 
+# The NUM_PROC_THREADS specifies the number threads doxygen is allowed to use
+# during processing. When set to 0 doxygen will based this on the number of
+# cores available in the system. You can set it explicitly to a value larger
+# than 0 to get more control over the balance between CPU load and processing
+# speed. At this moment only the input processing can be done using multiple
+# threads. Since this is still an experimental feature the default is set to 1,
+# which efficively disables parallel processing. Please report any issues you
+# encounter. Generating dot graphs in parallel is controlled by the
+# DOT_NUM_THREADS setting.
+# Minimum value: 0, maximum value: 32, default value: 1.
+
+NUM_PROC_THREADS       = 1
+
 #---------------------------------------------------------------------------
 # Build related configuration options
 #---------------------------------------------------------------------------
@@ -559,7 +574,7 @@ INTERNAL_DOCS          = NO
 # names in lower-case letters. If set to YES, upper-case letters are also
 # allowed. This is useful if you have classes or files whose names only differ
 # in case and if your file system supports case sensitive file names. Windows
-# (including Cygwin) ands Mac users are advised to set this option to NO.
+# (including Cygwin) and Mac users are advised to set this option to NO.
 # The default value is: system dependent.
 
 CASE_SENSE_NAMES       = NO
@@ -829,7 +844,11 @@ WARN_LOGFILE           =
 # spaces. See also FILE_PATTERNS and EXTENSION_MAPPING
 # Note: If this tag is empty the current directory is searched.
 
-INPUT                  = ..
+INPUT                  = ../spot_formula_to_dot.cpp \
+                         ../spot_checker.cpp \
+                         ../README.md \
+                         spot_formula_to_dot.md \
+                         spot_formula_to_dot.txt
 
 # This tag can be used to specify the character encoding of the source files
 # that doxygen parses. Internally doxygen uses the UTF-8 encoding. Doxygen uses
@@ -853,11 +872,10 @@ INPUT_ENCODING         = UTF-8
 # *.hh, *.hxx, *.hpp, *.h++, *.cs, *.d, *.php, *.php4, *.php5, *.phtml, *.inc,
 # *.m, *.markdown, *.md, *.mm, *.dox (to be provided as doxygen C comment),
 # *.doc (to be provided as doxygen C comment), *.txt (to be provided as doxygen
-# C comment), *.py, *.pyw, *.f90, *.f95, *.f03, *.f08, *.f, *.for, *.tcl, *.vhd,
+# C comment), *.py, *.pyw, *.f90, *.f95, *.f03, *.f08, *.f18, *.f, *.for, *.vhd,
 # *.vhdl, *.ucf, *.qsf and *.ice.
 
-FILE_PATTERNS          = spot_checker.cpp \
-                         README.md
+FILE_PATTERNS          =
 
 # The RECURSIVE tag can be used to specify whether or not subdirectories should
 # be searched for input files as well.
@@ -981,7 +999,7 @@ FILTER_SOURCE_PATTERNS =
 # (index.html). This can be useful if you have a project on for instance GitHub
 # and want to reuse the introduction page also for the doxygen output.
 
-USE_MDFILE_AS_MAINPAGE = README.md
+USE_MDFILE_AS_MAINPAGE = ../README.md
 
 #---------------------------------------------------------------------------
 # Configuration options related to source browsing
@@ -1089,10 +1107,13 @@ CLANG_ASSISTED_PARSING = NO
 CLANG_OPTIONS          =
 
 # If clang assisted parsing is enabled you can provide the clang parser with the
-# path to the compilation database (see:
-# http://clang.llvm.org/docs/HowToSetupToolingForLLVM.html) used when the files
-# were built. This is equivalent to specifying the "-p" option to a clang tool,
-# such as clang-check. These options will then be passed to the parser.
+# path to the directory containing a file called compile_commands.json. This
+# file is the compilation database (see:
+# http://clang.llvm.org/docs/HowToSetupToolingForLLVM.html) containing the
+# options used when the source files were built. This is equivalent to
+# specifying the "-p" option to a clang tool, such as clang-check. These options
+# will then be passed to the parser. Any options specified with CLANG_OPTIONS
+# will be added as well.
 # Note: The availability of this option depends on whether or not doxygen was
 # generated with the -Duse_libclang=ON option for CMake.
 
@@ -1362,7 +1383,7 @@ CHM_FILE               =
 HHC_LOCATION           =
 
 # The GENERATE_CHI flag controls if a separate .chi index file is generated
-# (YES) or that it should be included in the master .chm file (NO).
+# (YES) or that it should be included in the main .chm file (NO).
 # The default value is: NO.
 # This tag requires that the tag GENERATE_HTMLHELP is set to YES.
 
@@ -1524,6 +1545,17 @@ TREEVIEW_WIDTH         = 250
 
 EXT_LINKS_IN_WINDOW    = NO
 
+# If the HTML_FORMULA_FORMAT option is set to svg, doxygen will use the pdf2svg
+# tool (see https://github.com/dawbarton/pdf2svg) or inkscape (see
+# https://inkscape.org) to generate formulas as SVG images instead of PNGs for
+# the HTML output. These images will generally look nicer at scaled resolutions.
+# Possible values are: png (the default) and svg (looks nicer but requires the
+# pdf2svg or inkscape tool).
+# The default value is: png.
+# This tag requires that the tag GENERATE_HTML is set to YES.
+
+HTML_FORMULA_FORMAT    = png
+
 # Use this tag to change the font size of LaTeX formulas included as images in
 # the HTML documentation. When you change the font size after a successful
 # doxygen run you need to manually remove any form_*.png images from the HTML
@@ -1579,7 +1611,7 @@ MATHJAX_FORMAT         = HTML-CSS
 # Content Delivery Network so you can quickly see the result without installing
 # MathJax. However, it is strongly recommended to install a local copy of
 # MathJax from https://www.mathjax.org before deployment.
-# The default value is: https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.5/.
+# The default value is: https://cdn.jsdelivr.net/npm/mathjax@2.
 # This tag requires that the tag USE_MATHJAX is set to YES.
 
 MATHJAX_RELPATH        = https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.5/
@@ -1818,9 +1850,11 @@ LATEX_EXTRA_FILES      =
 
 PDF_HYPERLINKS         = YES
 
-# If the USE_PDFLATEX tag is set to YES, doxygen will use pdflatex to generate
-# the PDF file directly from the LaTeX files. Set this option to YES, to get a
-# higher quality PDF documentation.
+# If the USE_PDFLATEX tag is set to YES, doxygen will use the engine as
+# specified with LATEX_CMD_NAME to generate the PDF file directly from the LaTeX
+# files. Set this option to YES, to get a higher quality PDF documentation.
+#
+# See also section LATEX_CMD_NAME for selecting the engine.
 # The default value is: YES.
 # This tag requires that the tag GENERATE_LATEX is set to YES.
 
@@ -2059,6 +2093,10 @@ DOCBOOK_PROGRAMLISTING = NO
 
 GENERATE_AUTOGEN_DEF   = NO
 
+#---------------------------------------------------------------------------
+# Configuration options related to Sqlite3 output
+#---------------------------------------------------------------------------
+
 #---------------------------------------------------------------------------
 # Configuration options related to the Perl module output
 #---------------------------------------------------------------------------