플로트 타입이없는 합금 솔버

Question

저는 합금 문제를 작성하려고합니다. 여기에는 그 사이에 일련의 상태와 전환이 있습니다. 나의 목표는 주들 사이의 전환을 찾는 것입니다. 또한 각 상태 s는 이웃의 X 값을 사용하여 계산할 수있는 X (s) 값을 가지고 있으며 특정 값보다 작은 모든 값이 필요합니다. 내 문제는 합금이 부동을 지원하지 않으며 내 X 값이 정수가 아닐 수도 있다는 것입니다. 따라서, 함수 X를 상태에서 일부 숫자 유형으로 정의하려면 해당 유형은 Int 만 가능할 수 있습니다. 이 문제를 어떻게 해결할 수 있을까요?

도와 주셔서 감사합니다 많이 는 감사 Fathiyeh

Answer 1

내가 합금에 익숙하지 않은,하지만 하나 개의 일반 해는 정수를 사용하여 분수를 표현하기 위해 fixed-point arithmetic을 사용하는 것입니다. 예를 들어 값 1.23은 1/1000의 배율 인수를 사용하여 정수 1230으로 나타낼 수 있습니다. 물론 계산시이 스케일링 계수를 고려하여 필요한 경우 1000을 곱해야합니다.

Answer 2

정말 이웃들로부터 X를 계산하여 무엇을 의미하는지에 달려 있습니다.

X 위에 부동 소수점 연산을 적용해야합니까? 그렇다면 아마 Alloy에서 문제를 모델링 할 수 없을 것입니다.

단순한 산술 연산을 적용하려는 경우, 부동 소수점을 Alloy의 정수 표현에 매핑 할 수 있습니다. 이것은 또한 Alloy의 정수 범위가 한정되어 있으므로주의해서 처리해야합니다.

X 사이의 크기 순서를 비교하면 X를 추상 합금 서명으로 추상화하고 모듈 util/ordering을 사용하여 원자에 대한 순서를 정의하는 것이 가장 좋습니다.

Answer 3

vitaut가 말한 첫 번째 방법은 부동 소수점 수의 의미를 사용하는 것입니다. 부동 소수점 수는 부동 소수점 수 = 가수 x 지수 인 입니다.

모델링의 또 다른 방법은 왼쪽과 오른쪽에 숫자를 나타내는 2 개의 정수 - 2 개의 "필드"가있는 서명을 만드는 것입니다. 모양은 다음과 같습니다.

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