search

tnelson / FlowLog

17 stars 5 forks source link

Alloy compiler: underconstraint for forward, emit #32

Closed tnelson closed 10 years ago

tnelson commented 10 years ago

(1) If fields are left unmentioned in a forward rule, Alloy will just leave them unconstrained, rather than taking the default behavior (which is "leave unmodified").

(2) In an emit, Alloy will likewise leave unspecified fields unconstrained, rather than asserting that they must equal the default (if any).

These are serious soundness bugs in the compiler (i.e., Alloy can give scenarios that are impossible in practice, but will not miss additional possible scenarios).

adferguson commented 10 years ago

great work, Tim.

tnelson commented 10 years ago

This should now be fixed.