bppTool install z3 SMT solver and run "python3 checking.py" (Ubuntu) smt_generator.py: creates a python file named "constraint.py" and generates constraints on it definition.py: definition of temperal logic formulas structure.py: information from the inputs