alloy

0熱度

1回答

我已經使用合金模擬了我的項目，並且我想將運行部分與我的項目的建模部分分開。在一些事實和謂詞中，我使用add函數進行基數比較。下面是一個例子： #relation1 = add[ #(relation2), 1] 當運行部分和模型部分是在同一個文件中的所有成功運行。但是，當我在2個文件將它們分開，我有以下的語法錯誤： The name "add" cannot be found. 我認

2熱度

2回答

爲什麼可能合金負基數

我正在用合金語言描述一些模型。爲了描述一個有限狀態機我公司提供的代碼，這幾行： sig FSA_state { transitions: some FSA_state, initial: lone InitialState } sig InitialState {} fact i { all f: FSA_state | #(f.transitions)

0熱度

1回答

使用Alloy Models

我正在開發一個關於SA 論壇中間件中HA應用程序實時升級的項目。在我的部分研究中，我需要爲我的輸入升級活動文件製作一個UML配置文件，並驗證該文件是否存在某些依賴性約束。現在我想在我的工作中使用ALLOY 而不是UML，因爲它比UML更抽象和形式化。（當然UML + OCL將是正式的。）。現在我的問題是，如果UML + OCL是正式的，那麼使用ALLOY有什麼好處？一般來說，使用All

1熱度

2回答

隨機選取合金中的物體

假設您有一個在Alloy ... 中定義的基本電梯系統您在每層樓都有一組樓層和一組等待電梯的人。您可以與州一起顯示電梯的進度。你怎麼能把電梯在初始狀態下送到隨機樓去接他的第一個人？（又名;你如何隨機化元素合金需要？）

3熱度

1回答

解析從字符串

方法CompUtil.parseOneExpression_fromString含有的原子的表達提供了以下錯誤：名稱「原子$ 0」無法找到當解析的字符串包含含有一個原子的標籤的表達直。這可以理解，因爲單獨的原子不是直接在模塊級別定義，而是在實例查找過程中「生成」。但是！可以使用與Alloy Visualizer一起使用的控制檯評估器直接評估包含原子的表達式。那麼API中用於評估解決方案的方法

3熱度

1回答

Alloy - 從.als生成.xml實例

我需要從我的程序中的.als生成隨機.xml實例。我設法通過在後臺運行合金（隱形JFrame）並調用doOpen，doExecuteLatest和doShowLatest函數來實現這一點。但是每次運行我的代碼時都必須等待合金開始，這是一個痛苦。我認爲如果我簡單地使用這個程序的合金代碼部分（我想那將是kodkod）會更有效率。有誰知道該怎麼做？我發現合金的代碼很混亂...

2熱度

2回答

如何在給定的解決方案評估不同的模型不是用來生成aforementionned解決方案

假設一個聲明，我們有兩個模塊A和B，（A在B打開）您生成一個解決方案的謂詞來自A，並且在B中有一些參數化謂詞，只有關於A BUT的元素的原因，因爲某些原因，您不能將這些謂詞放在模塊A中。如何評估在從B生成的解決方案中聲明的謂詞一個？這裏有以下步驟我跟着來嘗試實現這一目標（失敗）生成一個的解決方案採用B 的所有可達簽名閱讀本解決方案解析爲一個表達式作爲基於A的參數檢索在B中聲明的謂詞

0熱度

2回答

是由合金支持的乘法和除法運算符嗎？

我想知道如果乘法和除法運算符是由Alloy支持的。我嘗試過乘法運算符「*」，但它不起作用。「+」的作品雖然。非常感謝。此致 Fathiyeh

1熱度

1回答

合金中的A4options對稱和簽名實例置換

我已經在Alloy中建立了圖表轉換鏈。我對解決問題的任何鏈條感興趣，但有些鏈條完全一樣。除了簽名實例之間的排列之外，它們是相同的，但實例之間的關係形成從一個解決方案到另一個解決方案完全相同的圖形。有沒有辦法避免這些冗餘解決方案？我在A4Option類中看到了一個對稱選項，但我真的不知道如何配置它。 /** This option specifies the amount of symmetr

0熱度

1回答

如何檢查兩個謂詞是否相等？

對於某些謂詞，我有兩種不同的實現方式，我想檢查它們是否都返回相同的實例，我如何執行此操作？謝謝。