alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

compression: fix bad encoding

Browse source 
Fixes #190.

* NEWS, spot/misc/intvcomp.cc: here.
This commit is contained in:
Etienne Renault 2016-10-25 14:12:50 +02:00
parent ce63c30c0b
commit f9991288f7
2 changed files with 7 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

3
NEWS
View file

@ -25,6 +25,9 @@ New in spot 2.1.2.dev (not yet released)
genltl --go-theta=12 | ltl2tgba --low --any genltl --go-theta=12 | ltl2tgba --low --any
is instantaneous as it should be. 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) New in spot 2.1.2 (2016-10-14)
Command-line tools: Command-line tools:

7
spot/misc/intvcomp.cc
View file

@ -22,6 +22,7 @@
#include <cstddef> #include <cstddef>
#include <cassert> #include <cassert>
#include <spot/misc/intvcomp.hh> #include <spot/misc/intvcomp.hh>
#include <iostream>
namespace spot namespace spot
{ {
@ -38,7 +39,7 @@ namespace spot
// 00 encodes "value 0" // 00 encodes "value 0"
// 010 encodes "value 1" // 010 encodes "value 1"
// 011 encodes "a value in [2..5]" followed by 2 bits // 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 // 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 // 110 encodes "repeat prev. value [9..40] times" followed by 5 bits count
// 111 encodes "an int value" followed by 32 bits // 111 encodes "an int value" followed by 32 bits
@ -74,14 +75,14 @@ namespace spot
self().push_bits(0x3, 3, 0x7); self().push_bits(0x3, 3, 0x7);
self().push_bits(val - 2, 2, 0x3); 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(0x4, 3, 0x7);
self().push_bits(val - 6, 4, 0xf); self().push_bits(val - 6, 4, 0xf);
} }
else else
{ {
assert(val > 22); assert(val > 21);
self().push_bits(0x7, 3, 0x7); self().push_bits(0x7, 3, 0x7);
self().push_bits(val, 32, -1U); self().push_bits(val, 32, -1U);
} }