|
|
|
SearchNavigationUser login |
Please help me solve this.
|
||||
The development of this site is supported by the National Science Foundation under Computing Research Infrastructure Grant No. 0707612.
Theme originally designed by Chris Herberte
You give a fact that defines Small exactly:
Small = One -> Two + Two ->Three + Three -> Four + Four -> Five
There is no One->Three in there, so unless Two=Three in all models of your specification (it does not) this will be false.
What you probably mean is
sig Number{smaller : Number}
one sig One, Two, Three, Four, Five extends Number{} // `one' to ensure a single atom for each; `extend' rather than `in' to make disjoint
fact smaller_definition{smaller = *(One -> Two + Two ->Three + Three -> Four + Four -> Five)}// transitive closure of kernel.
check {One->Three in smaller}
Jeremy L. Jacob Tel: +44-1904-43-2747 Fax: +44-1904-43-2767
Jeremy.Jacob@cs.york.ac.uk http://www-users.cs.york.ac.uk/~jeremy/
Dept. of Computer Science, The University of York, YORK, YO10 5DD, UK
I tried your specification, and it works for the relation One -> Three. But for the relation such as
check {Five -> Three in smaller}
Why it does not say the assertion is invalid?
The way I prefer to code your problem is:
enum Nat {One, Two, Three, Four, Five}
fun smaller : Nat -> Nat{*(One -> Two + Two ->Three + Three -> Four + Four -> Five):>Nat}
run{}
check {One->Three in smaller}
check {Three->One in smaller}
which does what you would expect.
Jeremy L. Jacob Tel: +44-1904-43-2747 Fax: +44-1904-43-2767
Jeremy.Jacob@cs.york.ac.uk http://www-users.cs.york.ac.uk/~jeremy/
Dept. of Computer Science, The University of York, YORK, YO10 5DD, UK