diff --git a/NEWS b/NEWS index 03cd9f9b6..02e580028 100644 --- a/NEWS +++ b/NEWS @@ -6,6 +6,9 @@ New in spot 2.3.0.dev (not yet released) will select the best output automaton for each formula translated. See https://spot.lrde.epita.fr/ltldo.html#portfolio for examples. + - The colors used in the output of ltlcross have been adjusted to + work better with white backgrounds and black backgrounds. + Library: - spot::twa_run::as_twa() has an option to preserve state names. diff --git a/bin/ltlcross.cc b/bin/ltlcross.cc index 0231391ea..5a55df9d3 100644 --- a/bin/ltlcross.cc +++ b/bin/ltlcross.cc @@ -197,9 +197,9 @@ static color_type const color_types[] = ARGMATCH_VERIFY(color_args, color_types); static color_type color_opt = color_if_tty; -static const char* bright_red = "\033[01;31m"; -static const char* bright_blue = "\033[01;34m"; -static const char* bright_yellow = "\033[01;33m"; +static const char* bright_red = "\033[1;31m"; +static const char* bold = "\033[1m"; +static const char* bold_std = "\033[0;1m"; static const char* reset_color = "\033[m"; static unsigned states = 200; @@ -242,7 +242,7 @@ static std::ostream& example() { if (color_opt) - std::cerr << bright_yellow; + std::cerr << bold_std; return std::cerr; } @@ -751,7 +751,7 @@ namespace err << "*Comp(P" << j << ')'; else err << "*N" << j; - err << " is nonempty; both automata accept the infinite word\n" + err << " is nonempty; both automata accept the infinite word:\n" << " "; example() << *w << '\n'; end_error(); @@ -914,7 +914,7 @@ namespace { std::cerr << "Trying to find a bogus mutation of "; if (color_opt) - std::cerr << bright_blue; + std::cerr << bold; std::cerr << bogus; if (color_opt) std::cerr << reset_color; @@ -946,13 +946,13 @@ namespace } std::cerr << "Smallest bogus mutation found for "; if (color_opt) - std::cerr << bright_blue; + std::cerr << bold; std::cerr << input; if (color_opt) std::cerr << reset_color; std::cerr << " is "; if (color_opt) - std::cerr << bright_blue; + std::cerr << bold; std::cerr << bogus; if (color_opt) std::cerr << reset_color; @@ -1018,7 +1018,7 @@ namespace if (filename || linenum) std::cerr << ' '; if (color_opt) - std::cerr << bright_blue; + std::cerr << bold; std::cerr << fstr << '\n'; if (color_opt) std::cerr << reset_color; diff --git a/doc/org/ltlcross.org b/doc/org/ltlcross.org index 66628a841..3afde30e9 100644 --- a/doc/org/ltlcross.org +++ b/doc/org/ltlcross.org @@ -617,23 +617,23 @@ positive and negative formulas by the ith translator). A single failing translator might generate a lot of lines of the form: - : error: P0*N1 is nonempty; both automata accept the infinite word + : error: P0*N1 is nonempty; both automata accept the infinite word: : cycle{p0 & !p1} - : error: P1*N0 is nonempty; both automata accept the infinite word + : error: P1*N0 is nonempty; both automata accept the infinite word: : p0; !p1; cycle{p0 & p1} - : error: P1*N1 is nonempty; both automata accept the infinite word + : error: P1*N1 is nonempty; both automata accept the infinite word: : p0; cycle{!p1 & !p0} - : error: P1*N2 is nonempty; both automata accept the infinite word + : error: P1*N2 is nonempty; both automata accept the infinite word: : p0; !p1; cycle{p0 & p1} - : error: P1*N3 is nonempty; both automata accept the infinite word + : error: P1*N3 is nonempty; both automata accept the infinite word: : p0; !p1; cycle{p0 & p1} - : error: P1*N4 is nonempty; both automata accept the infinite word + : error: P1*N4 is nonempty; both automata accept the infinite word: : p0; cycle{!p1 & !p0} - : error: P2*N1 is nonempty; both automata accept the infinite word + : error: P2*N1 is nonempty; both automata accept the infinite word: : p0; !p1; !p0; cycle{!p1 & !p0; p0 & !p1; !p1; !p1; p0 & !p1} - : error: P3*N1 is nonempty; both automata accept the infinite word + : error: P3*N1 is nonempty; both automata accept the infinite word: : p0; !p1; !p1 & !p0; cycle{p0 & !p1} - : error: P4*N1 is nonempty; both automata accept the infinite word + : error: P4*N1 is nonempty; both automata accept the infinite word: : p0; !p1; !p1 & !p0; cycle{p0 & !p1} In this example, translator number =1= looks clearly faulty @@ -799,39 +799,39 @@ true #+RESULTS: #+begin_example | & G ! p0 | ! p1 F ! p2 & & p1 G p2 F p0 -Running [P0]: modella 'lcr-i0-1XJw2X' 'lcr-o0-p2nbUW' -Running [N0]: modella 'lcr-i0-lSPMMV' 'lcr-o0-3xEoFU' +Running [P0]: modella 'lcr-i0-FUPmeY' 'lcr-o0-F3bZRp' +Running [N0]: modella 'lcr-i0-ebjQwR' 'lcr-o0-20eIbj' Performing sanity checks and gathering statistics... -error: P0*N0 is nonempty; both automata accept the infinite word +error: P0*N0 is nonempty; both automata accept the infinite word: cycle{!p0 & !p1} Trying to find a bogus mutation of (G!b & (!c | F!a)) | (c & Ga & Fb)... Mutation 1/22: & & p0 G p1 F p2 -Running [P0]: modella 'lcr-i1-3PI0CT' 'lcr-o0-GxBDAS' -Running [N0]: modella 'lcr-i1-eOijzR' 'lcr-o0-wkIZxQ' +Running [P0]: modella 'lcr-i1-zXEyXK' 'lcr-o0-RsypJc' +Running [N0]: modella 'lcr-i1-Ux7xvE' 'lcr-o0-x19Gh6' Performing sanity checks and gathering statistics... Mutation 2/22: & G ! p0 | ! p1 F ! p2 -Running [P0]: modella 'lcr-i2-6cYUzP' 'lcr-o0-3ihRBO' -Running [N0]: modella 'lcr-i2-6u8pEN' 'lcr-o0-phxZGM' +Running [P0]: modella 'lcr-i2-syS74x' 'lcr-o0-wPRySZ' +Running [N0]: modella 'lcr-i2-x9DdGr' 'lcr-o0-fgHStT' Performing sanity checks and gathering statistics... Mutation 3/22: | G ! p0 & & p1 G p2 F p0 -Running [P0]: modella 'lcr-i3-iwZZML' 'lcr-o0-LMB2SK' -Running [N0]: modella 'lcr-i3-r2g9ZJ' 'lcr-o0-HEfh7I' +Running [P0]: modella 'lcr-i3-rVOAil' 'lcr-o0-jU2i7M' +Running [N0]: modella 'lcr-i3-KATfWe' 'lcr-o0-2UOcLG' Performing sanity checks and gathering statistics... -error: P0*N0 is nonempty; both automata accept the infinite word +error: P0*N0 is nonempty; both automata accept the infinite word: cycle{!p0 & !p1} Trying to find a bogus mutation of G!b | (c & Ga & Fb)... Mutation 1/16: t -Running [P0]: modella 'lcr-i4-R8PbkI' 'lcr-o0-6ts7wH' -Running [N0]: modella 'lcr-i4-cv7EKG' 'lcr-o0-vVmdYF' +Running [P0]: modella 'lcr-i4-OJk2B8' 'lcr-o0-VVCSsA' +Running [N0]: modella 'lcr-i4-nKwTj2' 'lcr-o0-npMUau' Performing sanity checks and gathering statistics... Mutation 2/16: G ! p0 -Running [P0]: modella 'lcr-i5-ZO3HcF' 'lcr-o0-UiydrE' -Running [N0]: modella 'lcr-i5-gOseGD' 'lcr-o0-CL4fVC' +Running [P0]: modella 'lcr-i5-Waoe2V' 'lcr-o0-9wsyTn' +Running [N0]: modella 'lcr-i5-M0R2KP' 'lcr-o0-uhmxCh' Performing sanity checks and gathering statistics... Mutation 3/16: & & p0 G p1 F p2 @@ -839,10 +839,10 @@ warning: This formula or its negation has already been checked. Use --allow-dups if it should not be ignored. Mutation 4/16: | G ! p0 & p1 F p0 -Running [P0]: modella 'lcr-i6-QTDjtB' 'lcr-o0-tFpmKA' -Running [N0]: modella 'lcr-i6-1lnX1z' 'lcr-o0-TWWyjz' +Running [P0]: modella 'lcr-i6-OtIGuJ' 'lcr-o0-qBEQmb' +Running [N0]: modella 'lcr-i6-MGbcfD' 'lcr-o0-t93x74' Performing sanity checks and gathering statistics... -error: P0*N0 is nonempty; both automata accept the infinite word +error: P0*N0 is nonempty; both automata accept the infinite word: cycle{!p0 & !p1} Trying to find a bogus mutation of G!b | (c & Fb)... @@ -855,40 +855,40 @@ warning: This formula or its negation has already been checked. Use --allow-dups if it should not be ignored. Mutation 3/10: & p0 F p1 -Running [P0]: modella 'lcr-i7-CJTWjx' 'lcr-o0-DKbNEw' -Running [N0]: modella 'lcr-i7-tSts1v' 'lcr-o0-CGbWov' +Running [P0]: modella 'lcr-i7-4oa00w' 'lcr-o0-3IEsUY' +Running [N0]: modella 'lcr-i7-vyy5Nq' 'lcr-o0-nXOIHS' Performing sanity checks and gathering statistics... Mutation 4/10: | p0 G ! p1 -Running [P0]: modella 'lcr-i8-6dtbPu' 'lcr-o0-gLnsfu' -Running [N0]: modella 'lcr-i8-Xn6gGt' 'lcr-o0-U7966s' +Running [P0]: modella 'lcr-i8-Kt48Bk' 'lcr-o0-xeIzwM' +Running [N0]: modella 'lcr-i8-ye5are' 'lcr-o0-3QMMlG' Performing sanity checks and gathering statistics... Mutation 5/10: | G ! p0 F p0 -Running [P0]: modella 'lcr-i9-Vh7hAs' 'lcr-o0-eYZt3r' -Running [N0]: modella 'lcr-i9-I6dfxr' 'lcr-o0-DoY00q' +Running [P0]: modella 'lcr-i9-Bpmah8' 'lcr-o0-38lycA' +Running [N0]: modella 'lcr-i9-cQJ771' 'lcr-o0-yUcH3t' Performing sanity checks and gathering statistics... Mutation 6/10: | ! p0 & p1 F p0 -Running [P0]: modella 'lcr-i10-j7fVvq' 'lcr-o0-aChQ0p' -Running [N0]: modella 'lcr-i10-bnpgwp' 'lcr-o0-KV3G1o' +Running [P0]: modella 'lcr-i10-mYtDZV' 'lcr-o0-nCdAVn' +Running [N0]: modella 'lcr-i10-d1fIRP' 'lcr-o0-oAsQNh' Performing sanity checks and gathering statistics... -Mutation 7/10: | G p1 & p0 F p1 -Running [P0]: modella 'lcr-i11-uUhFyo' 'lcr-o0-OlrF5n' -Running [N0]: modella 'lcr-i11-XHjeDn' 'lcr-o0-0CINan' +Mutation 7/10: | & p1 F p0 G p0 +Running [P0]: modella 'lcr-i11-petsKJ' 'lcr-o0-Z3U4Gb' +Running [N0]: modella 'lcr-i11-bmFSDD' 'lcr-o0-P1DGA5' Performing sanity checks and gathering statistics... Mutation 8/10: | & p0 p1 G ! p0 -Running [P0]: modella 'lcr-i12-a7eJLm' 'lcr-o0-RUZFmm' -Running [N0]: modella 'lcr-i12-dobiYl' 'lcr-o0-LuVUzl' +Running [P0]: modella 'lcr-i12-eUjByx' 'lcr-o0-DZAwwZ' +Running [N0]: modella 'lcr-i12-v3JCur' 'lcr-o0-IzWIsT' Performing sanity checks and gathering statistics... Mutation 9/10: | G ! p0 & p0 F p0 -Running [P0]: modella 'lcr-i13-nFQYdl' 'lcr-o0-Mq84Rk' -Running [N0]: modella 'lcr-i13-CnPRwk' 'lcr-o0-7f4Fbk' +Running [P0]: modella 'lcr-i13-Sb2Arl' 'lcr-o0-kBwtqN' +Running [N0]: modella 'lcr-i13-Tctwpf' 'lcr-o0-hvIzoH' Performing sanity checks and gathering statistics... -error: P0*N0 is nonempty; both automata accept the infinite word +error: P0*N0 is nonempty; both automata accept the infinite word: cycle{!p0} Trying to find a bogus mutation of G!c | (c & Fc)... @@ -901,13 +901,13 @@ warning: This formula or its negation has already been checked. Use --allow-dups if it should not be ignored. Mutation 3/7: & p0 F p0 -Running [P0]: modella 'lcr-i14-KsKPgj' 'lcr-o0-Qo3UXi' -Running [N0]: modella 'lcr-i14-FVPvFi' 'lcr-o0-Zh06mi' +Running [P0]: modella 'lcr-i14-iDAoo9' 'lcr-o0-6vSdoB' +Running [N0]: modella 'lcr-i14-WMIdo3' 'lcr-o0-NxEdov' Performing sanity checks and gathering statistics... Mutation 4/7: | p0 G ! p0 -Running [P0]: modella 'lcr-i15-JB045h' 'lcr-o0-EIL4Oh' -Running [N0]: modella 'lcr-i15-sYY8yh' 'lcr-o0-KVOdjh' +Running [P0]: modella 'lcr-i15-lS5FoX' 'lcr-o0-XFX8op' +Running [N0]: modella 'lcr-i15-8IdNpR' 'lcr-o0-0Bxrqj' Performing sanity checks and gathering statistics... Mutation 5/7: | G ! p0 F p0 @@ -915,13 +915,13 @@ warning: This formula or its negation has already been checked. Use --allow-dups if it should not be ignored. Mutation 6/7: | ! p0 & p0 F p0 -Running [P0]: modella 'lcr-i16-hoqdSg' 'lcr-o0-xghJEg' -Running [N0]: modella 'lcr-i16-5JvOrg' 'lcr-o0-SUdVeg' +Running [P0]: modella 'lcr-i16-7boQrL' 'lcr-o0-wsIftd' +Running [N0]: modella 'lcr-i16-tk8OuF' 'lcr-o0-9wQow7' Performing sanity checks and gathering statistics... -Mutation 7/7: | & p0 F p0 G p0 -Running [P0]: modella 'lcr-i17-BNo92f' 'lcr-o0-0T8nRf' -Running [N0]: modella 'lcr-i17-J5v5Ff' 'lcr-o0-MOyNuf' +Mutation 7/7: | G p0 & p0 F p0 +Running [P0]: modella 'lcr-i17-wnlkyz' 'lcr-o0-MAjgA1' +Running [N0]: modella 'lcr-i17-qFLnCt' 'lcr-o0-45gvEV' Performing sanity checks and gathering statistics... Smallest bogus mutation found for (G!b & (!c | F!a)) | (c & Ga & Fb) is G!c | (c & Fc).