Alloy Analyzer 4.2 (mac) по сравнению с API сплава

В настоящее время я делаю программу, которая обрабатывает некоторые аннотации в java, а затем создает модель сплава, анализирует ее с помощью API сплава, а затем запускает некоторые команды сплава. Когда я тестирую сгенерированную модель сплава в приложении сплава, она работает нормально и дает ожидаемые результаты. Однако, когда я запускаю сгенерированную модель сплава через API, он говорит мне: «Вы должны указать область действия для sig this/ObjectName». Я прочитал код сплава из такой строки.

world = CompUtil.parseOneModule(String model);

Единственные варианты, которые я использую, — это решатель SAT4J и глубина skolem, равная 1.

Затем я перебираю команды из мира, перевожу их в кодкод и выполняю.

for(Command command: world.getAllCommands()) {
    A4Solution ans = null;
        try {
            ans = TranslateAlloyToKodkod.execute_command(rep, world.getAllReachableSigs(), command, options);
        } catch (Err ex) {
            Logger.getLogger(AlloyTest.class.getName()).log(Level.SEVERE, null, ex);
        }
}

Мой ОБНОВЛЕННЫЙ код сплава выглядит так:

module mvc
// General model
abstract sig Configuration { elements: set Element }
abstract sig Element { references: set Element }

// MVC Style
abstract sig Model extends Element { }
abstract sig View extends Element { }
abstract sig Controller extends Element { }

pred mvc_model_style [c: Configuration] {
all m: c.elements & Model | all r: m.references | r not in View
}
pred mvc_view_style [c: Configuration] {
all view: c.elements & View | all ref: view.references | ref not in Model
}

pred mvc_controller_style [c: Configuration] {
    all controller: c.elements & Controller | all ref: controller.references | ref in Model or ref in View or ref in Controller
}

pred mvc_style [c: Configuration]{
 mvc_model_style[c] mvc_view_style[c]
}
one sig testMvc extends Configuration { } {
elements = TestController + ViewTest + TestModel + TestController3
}
one sig TestController extends Controller { } {
references = TestController + TestModel
}
one sig ViewTest extends View { } {
references = TestController
}
one sig TestModel extends Model { } {
references = ViewTest + TestController3
}
one sig TestController3 extends Controller { } {
references = TestController + TestModel
}
assert testcontroller {
mvc_controller_style[testMvc]
}
assert viewtest {
mvc_view_style[testMvc]
}
assert testmodel {
mvc_model_style[testMvc]
}
assert testcontroller3 {
mvc_controller_style[testMvc]
}
check testcontroller for 8 but 1 Configuration
check viewtest for 8 but 1 Configuration
check testmodel for 8 but 1 Configuration
check testcontroller3 for 8 but 1 Configuration

Итак, кто-нибудь знает, как я могу это исправить, поскольку я думал, что для 1 конфигурации 8 элементов установят область действия для всех расширяющихся сигналов?

Редактировать*

Я обновил свою модель сплава с предложениями, и я все еще получаю ту же ошибку: «Вы должны указать область действия для sig« this/Controller ». Приведенный выше код сплава работает в анализаторе сплавов и дает следующий результат:

Executing "Check testcontroller for 8 but 1 Configuration"
   Solver=sat4j Bitwidth=0 MaxSeq=0 SkolemDepth=1 Symmetry=20
   83 vars. 26 primary vars. 98 clauses. 5ms.
   No counterexample found. Assertion may be valid. 1ms.

Executing "Check viewtest for 8 but 1 Configuration"
   Solver=sat4j Bitwidth=0 MaxSeq=0 SkolemDepth=1 Symmetry=20
   65 vars. 25 primary vars. 75 clauses. 5ms.
   No counterexample found. Assertion may be valid. 0ms.

Executing "Check testmodel for 8 but 1 Configuration"
   Solver=sat4j Bitwidth=0 MaxSeq=0 SkolemDepth=1 Symmetry=20
   65 vars. 25 primary vars. 75 clauses. 5ms.
   found. Assertion is invalid. 6ms.

Executing "Check testcontroller3 for 8 but 1 Configuration"
   Solver=sat4j Bitwidth=0 MaxSeq=0 SkolemDepth=1 Symmetry=20
   83 vars. 26 primary vars. 98 clauses. 6ms.
   No counterexample found. Assertion may be valid. 0ms.

alloy
person Asger Pedersen    schedule 26.01.2013    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Ваша модель Alloy содержит синтаксические ошибки, поэтому вы также не можете запустить ее с помощью анализатора Alloy.

Прежде всего, правильный способ указать область проверки вашего testcontroller таков:

check testcontroller for 8 but 1 Configuration

Это означает «для 8 атомов всего, но 1 атом конфигурации», тогда как то, что вы написали, не анализирует события.

Далее, предикат mvc_controller_style не определен, что также вызовет у вас проблемы.

Что касается вашего использования API, просто измените parseOneModule на parseEverything_fromFile, и все должно работать. Я также ожидал бы, что parseOneModule будет работать в этом случае (потому что в вашей модели только один модуль), но это просто не так, потому что по какой-то причине некоторые имена не разрешаются должным образом. Я не уверен, является ли это ошибкой или, может быть, этот метод не должен быть частью общедоступного API. Во всяком случае, вот мой код, который правильно работал для вашего примера:

public static void main(String[] args) throws Exception {
    A4Reporter rep = new A4Reporter();

    Module world = CompUtil.parseEverything_fromFile(rep, null, "mvc.als");
    A4Options options = new A4Options();
    options.solver = A4Options.SatSolver.SAT4J;
    options.skolemDepth = 1;

    for (Command command : world.getAllCommands()) {
        A4Solution ans = null;
        try {
            ans = TranslateAlloyToKodkod.execute_commandFromBook(rep, world.getAllReachableSigs(), command, options);
            System.out.println(ans);
        } catch (Err ex) {
            Logger.getLogger(AlloyTest.class.getName()).log(Level.SEVERE, null, ex);
        }
    }
}
person Aleksandar Milicevic    schedule 26.01.2013
comment
Спасибо за ответ, но я все еще получаю ту же ошибку при использовании API. Я обновил свой вопрос. - person Asger Pedersen; 27.01.2013
comment
Да, я изменил его, чтобы использовать parseEverything_fromFile, и теперь он работает. Спасибо - person Asger Pedersen; 28.01.2013
comment
Я бы предложил использовать execute_command в качестве Асгера Педерсена вместо execute_commandFromBook: последний также загружает все примеры из книги Дэниела Джексона. - person Pietro Braione; 18.12.2014