1

I'm new to the Alloy API and I'm currently trying to implement my own serializer for Alloy solutions. What I've basically done is:

  • I've written an Alloy model that contains the signatures A, B, C, D and E
  • A has a field
  • B is abstract
  • C has a ternary relation tr: A -> lone B
  • D and E extend B and are not abstract

The model is evaluated by the solver and provides the desired solutions. What I now want to do is to use a custom serialization format (just for information: it is called XES http://www.xes-standard.org/).

My question now is: In order to retrieve the required information for the serialization format, I need all elements which have the signature C and includes a tuple (A,D). How can I search for custom elements in the solution?

Thank you very much in advance, LostSpirit

LostSpirit
  • 23
  • 3

1 Answers1

2

You can use the Alloy API that provides methods to:

  • Get an A4Solution object out of an instance obtained by analysis of a given model (check the A4Reader class),
  • Go through all the atoms of the solution (check A4Solution class)
  • Get a CompModule object out of an Alloy module (check CompUtil Class)
  • Evaluate the fields of this compmodule in the A4Solution obtained in point 1. (in order to get the tuples present in the solution)

Check the answer to this question, it's quite related to yours:

going through an A4Solution

Community
  • 1
  • 1
Loïc Gammaitoni
  • 4,173
  • 16
  • 39