Barnard-PL-Labs / tsltools

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

Error posix_spawnp: does not exist #67

Closed w14 closed 11 months ago

w14 commented 11 months ago

To reproduce:

tsl synthesize the following TSL spec:

always guarantee {
    [y <- y + 1] || [y <- 0];
    y = 5 -> X y = 0;
}

This looks realizable to me, because you can just always set y = 0.

leoqiao18 commented 11 months ago

This is because TSLMT synthesis procedure uses CVC5 internally. We should add a more helpful error message (i.e. check for the availability of CVC5 before using it).

leoqiao18 commented 11 months ago

Added check for solver path in commit cfb2d87921f8b15080c790bf5556dd04685d622f