Barnard-PL-Labs / tsltools

Library and tools for the TSL specification format
Other
7 stars 4 forks source link

add support for smaller decimals #41

Closed ravenrothkopf closed 1 year ago

ravenrothkopf commented 1 year ago

this spec

always assume{

}
always guarantee{
    [x <- x + 0.01];
}

generates

Command failed: ./tslsynth tmp.tsl --js
"Syntax Error" (line 1, column 59):
unexpected ")"
expecting "(", "{", "|", "otherwise", "false", "true", "_", digit, "[" or identifier

but 0.1 and larger runs fine

leoqiao18 commented 1 year ago

This issue comes from the implementation of the Show instance for Value in Preprocessor.hs. It is using show r to turn it into a string (line 120).

A real like 0.01 gets turned into 1.0e-2. Therefore, the encoding after the preprocessing becomes real1.0e-2(), which becomes invalid syntax for TSL synthesis.

leoqiao18 commented 1 year ago

Fixed in PR #42