PLCverif — Verification report

Verification stages

Phase	Result	Runtime
Parsing source code	Successful	0 ms
Control-flow declaration generation	Successful	153 ms
Requirement representation	Successful	37 ms
Reductions (CFD)	Successful	66 ms
Model preparation	Successful	21 ms
Reductions (CFI)	Successful	53 ms
NuSMV model building	Successful	3 ms
NuSMV execution	Successful	250623 ms
NuSMV output parsing	Successful	0 ms
Result diagnosis	Successful	0 ms
Reporting	Unknown

Log

Message

Severity

Stage

Verification tool outputs

STDERR

STDOUT

*** This is NuSMV 2.6.0 (compiled on Wed Oct 14 15:37:51 2015)
*** Enabled addons are: compass
*** For more information on NuSMV see <http://nusmv.fbk.eu>
*** or email to <nusmv-users@list.fbk.eu>.
*** Please report bugs to <Please report bugs to <nusmv-users@fbk.eu>>

*** Copyright (c) 2010-2014, Fondazione Bruno Kessler

*** This version of NuSMV is linked to the CUDD library version 2.4.1
*** Copyright (c) 1995-2004, Regents of the University of Colorado

*** This version of NuSMV is linked to the MiniSat SAT solver.
*** See http://minisat.se/MiniSat.html
*** Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
*** Copyright (c) 2007-2010, Niklas Sorensson

Output to file: C:\Users\andia\AppData\Local\Temp\PLCverif-output3697846363106425651\case36.smv.cex


Plug-in key-value store

• nusmv$expression_type = Ctl

Effective settings used for the verification

-description = ""
-id = case36
-job = verif
-job.backend = nusmv
-job.backend.algorithm = Classic
-job.backend.binary_path = C:\Users\andia\Egyetem\nusmv\bin\NuSMV.exe
-job.backend.df = true
-job.backend.dynamic = true
-job.backend.locref_req_strategy = false
-job.backend.req_as_invar = false
-job.backend.timeout = 600
-job.reporters.0 = html
-job.reporters.0.hide_internal_variables = true
-job.reporters.0.include_settings = true
-job.reporters.0.include_stack_trace = false
-job.reporters.0.min_log_level = Warning
-job.reporters.0.show_logitem_timestapms = false
-job.reporters.0.show_verification_console_output = true
-job.reporters.0.use_lf_value_representation = false
-job.reporters.1 = summary
-job.req = pattern
-job.req.pattern_id = pattern-invariant
-job.req.pattern_params.1 = instance.outputs_match
-lf = step7
-lf.compiler = Step7v55
-lf.entry = aggr_36
-name = ""
-output = C:\Users\andia\AppData\Local\Temp\PLCverif-output3697846363106425651
-reductions.0 = basic_reductions
-reductions.0.ExpressionPropagation_maxage = 50
-reductions.0.ExpressionPropagation_maxexprsize = 100
-reductions.0.ExpressionPropagation_maxlocations = 50000
-reductions.0.fine_logging = false
-reductions.0.print_vardep_graph = false
-reductions.0.show_progress = false
-sourcefiles.0 = C:\Users\andia\Egyetem\student-serban-bsc\tdk-latex\src\attachments\examples\PLCverif\example_14.scl
-sourcefiles.1 = C:\Users\andia\Egyetem\student-serban-bsc\tdk-latex\src\attachments\examples\PLCverif\example.scl
-sourcefiles.2 = C:\Users\andia\Egyetem\student-serban-bsc\tdk-latex\src\attachments\examples\PLCverif\example_10.scl
-sourcefiles.3 = C:\Users\andia\Egyetem\student-serban-bsc\tdk-latex\src\attachments\examples\PLCverif\example_34.scl
-sourcefiles.4 = C:\Users\andia\Egyetem\student-serban-bsc\tdk-latex\src\attachments\examples\PLCverif\example_12.scl
-sourcefiles.5 = C:\Users\andia\Egyetem\student-serban-bsc\tdk-latex\src\attachments\examples\PLCverif\example_36.scl
-sourcefiles.6 = C:\Users\andia\Egyetem\student-serban-bsc\tdk-latex\src\attachments\examples\PLCverif\common.scl
-sourcefiles.7 = C:\Users\andia\Egyetem\student-serban-bsc\tdk-latex\src\attachments\examples\PLCverif\test.scl
-sourcefiles.8 = C:\Users\andia\Egyetem\student-serban-bsc\tdk-latex\src\attachments\examples\PLCverif\example_17.scl