search

GaloisInc / salty

A DSL for generating GR(1) problems
BSD 3-Clause "New" or "Revised" License
11 stars 3 forks source link

Liveness not translated to slugs correctly #16

Open lhumphrey opened 5 years ago

lhumphrey commented 5 years ago

It appears that when salty translates liveness properties, it conjoins them together in a single line in its input to slugs. However, separate liveness properties conjoined onto the same line do not have the same meaning. That is, the following are not equivalent: []<>(s1 /\ s2) []<>(s1) /\ []<>(s2)

The attached zip file contains a small example with 2 liveness properties. The structuredslugs and salt files are almost certainly equivalent (required only a very simple translation). The slugsin file is generated from the structuredslugs file using slug's tools/compiler.py, and I believe it is a correct translation. If you run salty like this: salty --ddump-spec running_lights2.salt

You can see that sys_liveness is & ! state1_3 ! state2_4 Instead of ! state1_3 ! state2_4 as it is in slugs.

You can comment out either one of the two sys_liveness properties in the salt file, and it becomes realizable.

There are also differences in the sys_trans section, but these may be equivalent.

runningLights2.zip

elliottt commented 5 years ago

It looks like there's only one sys_liveness section in the spec you attached. If you split it into separate sys_liveness sections, that should resolve the problem.

...
sys_liveness
  !state1

sys_liveness
  !state2
elliottt commented 5 years ago

Also, it's likely that the sys_trans section changed due to optimizations applied before writing out the slugs spec. The should be equivalent, and if they're not it's a bug.

lhumphrey commented 5 years ago

Thanks Trevor! I seem to remember some conversation about this now. This is interesting though. Slugs interprets liveness properties s1 and s2 one per line to be conjuncted outside the temporal operators like []<>s1 /\ []<>s2. And Salty wants multiple sys_liveness sections in order to consider them conjuncted in this way. I hadn't fully realized this.

I rechecked the paper, and it's kind of ambiguous with the way it's worded, so now I'm debating whether it makes more sense to do it the way we're doing it now or the way slugs does it. I think the way slugs interprets it (multiple lines are conjuncted outside the temporal operators) is the more common paradigm in other tools (not just Slugs).

Thoughts?

elliottt commented 5 years ago

It's a tough call. I liked having one sys_liveness block correspond to a single liveness property, as you're then free to break it up over multiple lines if that makes it easier to read. However, it's also nice to have it correspond more directly to what slugs expects as input.

Given that salty was meant to ease usage of slugs, I'd say it's up to you. If it's more intuitive to have sys_liveness properties be an implicit disjunction, then that's probably a good change to make.