Joachim Klein
05e7aedd95
prism-auto: tweak exit code handling in --verbose-test mode
If --verbose-test is on, we want to also count failure exit codes
from the PRISM calls as failures.
8 years ago
Joachim Klein
c32cde62cf
prism-auto: it's an error when file specified via -a/--args does not exist
8 years ago
Joachim Klein
491d05d4fa
prism-auto: flush() to align script with prism output when used with pipes
In non-test mode, PRISM and prism-auto both write to stdout, without
prism-auto seeing/processing the output of PRISM. If the output of
prism-auto is piped to another program or to a file, the prism-auto
output is buffered. Then, the output by prism-auto (e.g., printing the
command lines) is not properly synchronized with the output of the
PRISM instances.
So, we flush stdout at appropriate locations.
Additionally, on timeout we prepend a '\n' to ensure that the timeout
message starts at a new line (in particular for the common case of a
timeout during explicit model building, where there is no newline from
PRISM until the model is fully built).
8 years ago
Joachim Klein
55d7351994
prism-auto: --timeout n
Switch for doing timeouts. Using the PRISM -timeout mechanism does not work
nicely with nailgun, so we add a mechanism to prism-auto.
8 years ago
Joachim Klein
f1378fab52
prism-auto: --skip-duplicate-runs
When using -x to add additional options, i.e., to force a specific engine,
often runs of PRISM are effectively duplicated, e.g., if there are .args files
that select multiple engines.
Using the --skip-duplicate-runs, prism-auto tries to clean up the argument list,
remove switches that don't have an effect and to detect duplicate runs, only actually
executing the first one.
8 years ago
Joachim Klein
9bf1813160
prism-auto: --skip-export-runs
Option to allow skipping PRISM runs that do exports.
This is useful when overriding the engine, as the exports differ slightly
between engines and some export options are not supported.
8 years ago
Joachim Klein
36f895a597
prism-auto: Derive ngprism location from --prog setting
In nailgun mode, if --ngprism is not specified, we derive the location of the ngprism
binary from the --prog setting: We simply replace the file part with ngprism, as usually
the ngprism binary is located in the same directory as the prism startup script.
8 years ago
Joachim Klein
6452975791
prism-auto: fix printing of warnings in --verbose-test mode
Previously, if --verbose-test was active, the 'Warning: ...' lines
in the log were not printed.
8 years ago
Joachim Klein
1e39f308f4
prism-auto: count warnings, even if -w / --show-warnings is not active
8 years ago
Joachim Klein
fdacf84b2f
prism-auto: in nailgun mode, try to stop existing server first
Sometimes, if the prism-auto scripts gets interrupted, an existing
nailgun server is not properly shut down and might break a subsequent
prism-auto run.
8 years ago
Joachim Klein
482d47c458
prism-auto: fix compilation issue (whitespace) under python3
8 years ago
Joachim Klein
a899939687
prism-auto: fix broken incrementing of warning statistics
typo in the key string used for the counter dict
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12205 bbc10eb1-c90d-0410-af57-cb519fbb1720
8 years ago
Joachim Klein
c239ba7a6d
prism-auto: allow use of ngprism on Windows
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12198 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
Joachim Klein
a74d6b9841
prism-auto: refactor temporary log file handling to allow ngprism to work on Windows
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12197 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
Joachim Klein
ed01390e40
prism-auto: integrate warning for missing files (export check) into warning tracking / colour printing
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12194 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
Joachim Klein
8e461dd4c2
prism-auto: add --verbose-test (prints PRISM output but highlights test results and provides statistics like --test)
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12048 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
Dave Parker
a37e37679a
prism-auto: Slight tweak to colours and order of test outcomes.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12042 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
Joachim Klein
3dd1680c6e
prism-auto: count warnings / dd-warnings as well for statistic
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12004 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
Joachim Klein
c34d68046e
prism-auto: slight refactoring of colour printing
(1) use dedicated printColoured method, which suppresses
colouring if isColourEnabled() is false (e.g., when piping to a file)
(2) use dedicated colour (light red) for warnings, as before
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12003 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
Dave Parker
fe76535b3d
prism-auto: Add colour coding to summary table for passed/failed/etc. counts.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12000 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
Joachim Klein
5c21a80d68
prism-auto: print test statistics at the end if in test-mode
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11995 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
Dave Parker
d08a8d4c33
prism-auto fix: when checking output files in test mode, fail immediately when the first one is different.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11983 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
Dave Parker
751e95fa42
Small fix in prism-auto: make sure directory is passed to bench to benchmark function in "build" mode, in particular so that log names are created consisently. (Reported by Steffen Marcker).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11964 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
Joachim Klein
1e5d779cb3
prism-auto: In test mode, cleanup the temporary files used for capturing PRISM output
Due to the use of NamedTemporaryFile(delete=False) we actually have to
delete the log files ourselves.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11881 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
Joachim Klein
b203d6438d
prism-auto: Use line ending agnostic file compare
The previously used filecmp.cmp opens the files to be compared in 'rb'
mode, i.e., it will tell us that two files that differ only in the
line-ending encoding (CRLF vs LF) are not equivalent. However, we'd
like to get the export tests to succeed on Windows, regardless of the
line endings. So, we provide our own file comparison method that opens
the file in 'rU' mode (universal newline mode), which converts all the
newline encodings to '\n' transparently.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11880 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
Joachim Klein
fe533db326
prism-auto: Fix test-mode on Windows
Somehow, PRISM can not open a NamedTemporaryFile created on Windows
(see issue prismmodelchecker/prism#11 ) when passed the filename via
the -mainlog parameter.
So, on Windows, we fall back on the old method of capturing stdout
directly via the Popen call. As this does not work with nailgun (the
C printfs go to the nailgun server stdout), we currently don't allow
nailgun use on Windows.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11879 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
Joachim Klein
eb5028dbf8
prism-auto: add --dd-warnings mode for printing the CUDD reference leak warnings
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11812 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
Dave Parker
0f9dfe0275
prism-auto: Make sure nailgun is closed down if the script ends with an error (and refactor the exit code).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11743 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
Dave Parker
2a38cf110b
prism-auto: Don't actually execute nailgun commands in echo mode - just print them.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11742 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
Joachim Klein
2ff89c09a4
prism-auto: color 'NOT TESTED' test result just like 'SKIPPED'
NOT TESTED is the result of a // RESULT: ? line in a property file
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11599 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
Joachim Klein
79e5f3b68d
prism-auto: don't expand to filename for exports if 'stdout'
PRISM recognizes the filename 'stdout' as special and exports
to standard output, so prepending a directory by prism-auto
does not make sense.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11592 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
Joachim Klein
e838330aae
reapply previous commit (prepare prism-auto for python3 compatibility)
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11158 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Joachim Klein
e18c7362be
temporarily reverting previous commit (to figure out some Jenkins build stuff)
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11157 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Joachim Klein
4b711fe98a
prism-auto: add parentheses for print call to make script compatible with python3
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11155 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Dave Parker
b6828a7045
Remove unused "techLog" from Prism object and other classes.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11078 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Dave Parker
b7a034bb85
Remove changes accidentally commited in rev 10595.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10599 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Dave Parker
0f9e001645
Bug fix in CNF conversion (from Yuyang).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10595 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Dave Parker
5156f2d9c5
Fix in previous improvement to prism-auto.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10594 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Dave Parker
33e745af83
prism-auto: Location of ngprism can optionally be specified with --ngprism.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10593 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Dave Parker
6dd6628f52
Preliminary Nailgun support for prism-auto (add --nailgun).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10592 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Joachim Klein
3da87f5bf5
prism-auto: support multiple -x arguments
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10570 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Dave Parker
f601843c59
prism-auto bug fix (crashes when run on a single model in build mode).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10491 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
264ee2c080
prism-auto: revert previous commit, can not pass arguments to python when using env
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10444 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
a0f45900be
prism-auto: use -u switch to set stdout/stderr to unbuffered
As a side-effect, this sets stdout/stderr to 'binary', which might
make a difference on Windows...
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10442 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Dave Parker
500147ede4
prism-auto: Add -w/--show-warnings switch to show warnings (as well as errors) when in test mode.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10309 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Dave Parker
b5320f599d
prism-auto: Redirect PRISM techLog as well as mainLog (e.g. for CUDD warnings) when in test mode.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10308 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Dave Parker
c456da3455
prism-auto: Use -mainlog switch for redirecting output in test/log modes (mainly because this works better with Nailgun).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10303 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Dave Parker
f927684aba
prism-auto: --help tidy.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10257 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Dave Parker
952e550be7
prism-auto: Colour coding can be switched on/off with --colour switch (yes,no,auto).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10256 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Dave Parker
308ee00e64
prism-auto: Commenting
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10255 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago