1

I am trying to write an Alloy problem, in which I have a set of states and transitions between them. My goal is to find the transitions among states. Also, each state, s, has a value called X(s) that can be calculated using the X value of its neighbours, and I need all values of X to be less than a specific value. My problem is that Alloy does not support float, and my X values might not be Int. So, if I want to define a function X from states to some numeric type, that type can only be Int. Can you think of any way to go around this?

Thanks a lot for your help, Sincerely, Fathiyeh

3 Answers 3

1

That really depends on what you mean by calculating X from its neighbors.

Will you need to apply float-specific operations over X? If so, you probably won't be able to model your problem in Alloy.

If instead you just expect to apply simple arithmetic operations, you can try to map your floats to an integer representation in Alloy. This should also be handled with care as the range of integers in Alloy is bounded.

Better yet, if you just need to compare orders of magnitude between X's, you best bet is to abstract X to a generic Alloy signature and define an order over its atoms using the module util/ordering.

0

I am not familiar with Alloy, but one general solution is to use fixed-point arithmetic to represent fractional numbers using integers. For example, the value 1.23 can be represented as integer 1230 using a scaling factor of 1/1000. You'll need to take this scaling factor into account in your calculations of course, multiplying by 1000 where necessary.

0

Well first approach as mentioned by vitaut is to make use of the semantics of floating point numbers which is floating_point_number = mantissa x exponent.

Another way of modeling it would be creating a signature that has 2 "fields" - 2 integers representing numbers on left and right side. It can look like this

sig Float{
    leftPart: one Int,
    rightPart: one Int
}

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.