alloy

0열

1답변

주어진 인스턴스에 대한 모델 사양을 생성 할 수 있는지 궁금합니다. 내 목표는 인스턴스가 모델을 준수하는지 여부를 확인하는 것입니다. 사례의 자동 사양을 다루는 문서를 발견했습니다. 이를 '인스턴스를 사용하여 합금 사양을 작성하는 자동화 된 접근법'(http://users.ece.utexas.edu/~khurshid/papers/2006/06isola-aD

0열

1답변

합금의 두 표현식의 차이점은 무엇입니까?

한다고 가정 우리는 다음과 같은 합금 모델이 있습니다 내가 사라 년생 어떤 신입생와 호환되지 않을해야한다는 것을 말하고 싶은 abstract sig Season {} one sig Spring, Summer, Fall, Winter extends Season {} abstract sig Student { bornIn: one Season }

0열

1답변

두 관계의 조인과 세 관계의 조인에 대해 왜 동일한 그래픽을 얻습니까?

이하 이름, 주소 및 호스트의 세 가지 세트를 만듭니다. 주소 필드는 이름을 주소로 매핑합니다. 호스트 필드는 주소를 호스트로 맵핑합니다. sig Name { addr: Address } sig Address { host: Host } sig Host {} 여기에서는 합금 분석기에 addr과 host의 두 조인에 대한 인스턴

0열

1답변

제한된 Person에서, 아버지가없는 사람이 있어야합니다. 맞습니까?

다음 모델은 사람과 그 아버지를위한 모델입니다. "사실"은 어떤 사람도 자신의 아버지가 될 수 없으며 사람이 아버지의 아버지, 아버지의 아버지 등이 될 수 없다고 말합니다. "주장하다"는 말에는 모든 사람에게 아버지가 있다는 것입니다. "check"명령은 반올림 분석기가 반례를 찾도록 요청합니다. "체크"명령에는 경계가 지정되지 않습니다. 따라서 분석기는

0열

1답변

Visualizer가 모든 원자가 숨겨져 있다고 말하는 이유는 무엇입니까?

다음은 사람과 그 아버지의 모델입니다. Alloy Analyzer가 모델의 인스턴스를 보여주기를 원합니다. Alloy 도구에서 Execute 메뉴의 "Run Show"를 선택합니다. 그런 다음 '표시'버튼을 선택합니다. 여기에 비주얼이 표시 내용은 다음과 같습니다 나는 그게 무슨 뜻인지 모르는 . 나는 Theme을 클릭했고 나는 원자를 "숨기기"하는 데 도

1열

1답변

"설정"은 기본 다중도입니까?</p>입니다 <pre><code>r: A -> B r: A set -> set B </code></pre> <p>이 <code>set</code> 기본 다양성이다 :

이 두 동등? 그렇다면 소프트웨어 추상화 (Software Abstractions) 책에서 화살표 연산자의 정의에 대해 생각해 보겠습니다. 이 책은 55 페이지 말한다 :이 개 관계 p와 q의 화살표 제품 (또는 제품) P-> q는 당신이 튜플 페이지에서와 튜플의 모든 조합을 취함으로써 얻을 관계 q에서 가져 와서 연결하십시오. 난 Q는 Q 튜플과 P에서

1열

1답변

합금 및 코닥 (Kodkod)의 전체 주문 순서 최적화

분석의 효율성을 높이기 위해 총 주문 관계가 고정되어 있으며 ("012"에서 나타나는 원자 이름을 얻으려면 여러 곳에서 (예 : 여기 enter link description here 또는 there) 자연 "질서). 내가 이해하는 한, 최적화는 Kodkod (in this piece of code)에서 이루어집니다. 그러나 Java 문서보다 부울 행렬에

0열

1답변

중계 평등 올바르지 않은 것 같습니다.

~. r은 소프트웨어 추상화의 638 페이지에서과 같습니다. 올바르지 않은 것 같습니다. 나는 s ~ ~ r이 ~ (r. ~ s)와 같다고 믿는다.이 정확한 진술이다.

1열

1답변

합금의 서명 수에 제한이있는 명령 실행 동작

첫 번째 코드는 Alloy Analyzer 4.2에서 인스턴스를 찾을 수 없었지만 두 번째 인스턴스는 잘 찾았습니다! 차이점은 무엇입니까? 내 기대는 #> 0과 # = 1은 "show for 1"을 실행할 때 같은 역할을한다는 것이다. 1 : sig Fruit {} pred show() { #Fruit > 0} run show for 1 2 : 당신

0열

1답변

이 제약 조건을 표현하는 방법 : 둘 이상의 밴드에 가수가 있습니다.

이 제약 조건을 표현하고 싶습니다. 둘 이상의 밴드에 가수가 있습니다. 다음은 Band 및 Singer를 선언합니다. 관계 '밴드'는 가수를 밴드에 매핑합니다. sig Band {} sig Singer { band: Band } 이 원하는 제약 조건을 표현하기 위해 나타납니다 some s: Singer | some s.band 반사되면