From f9991288f79dd5902f1c3763daaa5881ba2b55c2 Mon Sep 17 00:00:00 2001 From: Etienne Renault Date: Tue, 25 Oct 2016 14:12:50 +0200 Subject: [PATCH] compression: fix bad encoding Fixes #190. * NEWS, spot/misc/intvcomp.cc: here. --- NEWS | 3 +++ spot/misc/intvcomp.cc | 7 ++++--- 2 files changed, 7 insertions(+), 3 deletions(-) diff --git a/NEWS b/NEWS index 0842834c4..8ea8c715b 100644 --- a/NEWS +++ b/NEWS @@ -25,6 +25,9 @@ New in spot 2.1.2.dev (not yet released) genltl --go-theta=12 | ltl2tgba --low --any is instantaneous as it should be. + * Compression could encode '6' and '22' in the same way. This issue + only appears when using the compression from intvcomp.hh. + New in spot 2.1.2 (2016-10-14) Command-line tools: diff --git a/spot/misc/intvcomp.cc b/spot/misc/intvcomp.cc index 3761d5ad6..cf2486455 100644 --- a/spot/misc/intvcomp.cc +++ b/spot/misc/intvcomp.cc @@ -22,6 +22,7 @@ #include #include #include +#include namespace spot { @@ -38,7 +39,7 @@ namespace spot // 00 encodes "value 0" // 010 encodes "value 1" // 011 encodes "a value in [2..5]" followed by 2 bits - // 100 encodes "a value in [6..22]" followed by 4 bits + // 100 encodes "a value in [6..21]" followed by 4 bits // 101 encodes "repeat prev. value [1..8] times" followed by 3 bits count // 110 encodes "repeat prev. value [9..40] times" followed by 5 bits count // 111 encodes "an int value" followed by 32 bits @@ -74,14 +75,14 @@ namespace spot self().push_bits(0x3, 3, 0x7); self().push_bits(val - 2, 2, 0x3); } - else if (val >= 6 && val <= 22) + else if (val >= 6 && val <= 21) { self().push_bits(0x4, 3, 0x7); self().push_bits(val - 6, 4, 0xf); } else { - assert(val > 22); + assert(val > 21); self().push_bits(0x7, 3, 0x7); self().push_bits(val, 32, -1U); }