Translation Electrum to NuSMV

1

Hi,

when using the Kodkod Engine with Alloy I can inspect the generated Kodkod code by clicking on “predicate” after running a specification. How can I get the generated NuSMV input when using the unbounded model checker NuSMV?

Or: how is the translation from Alloy/Electurm to NuSMV done? I think NuSMV expects as input a transition system, an instance. But in Alloy/Electrum there may be several instances for the same specification, how is this handled in the translation to NuSMV.
There is a short section about that topic in the paper of Nuno Macedo et al: Lightweight Specification …, but since I’m not so familiar with NuSMV, I don’t understand how NuSMV can handle a set of transition systems, not just one of them.

Thanks for any hints that can improve my understanding.

Kind regards,
Burkhardt Renz

2

Hi,
things have changed a bit since the cited paper was published.

On SMV files

Now, Electrum relies on Pardinus, a temporal extension of Kodkod. When solving with NuSMV or nuXmv, Pardinus sends its output to a compiler named Electrod, which takes care of (1) producing an SMV file, (2) passing it to NuSMV or nuXmv, (3) interpreting the result and (4) passing it back to Pardinus.

Zooming in the solving part, Electrod takes as input a Pardinus problem and generates an SMV file. The former can be retrieved as an .elo file in the directory of temporary files (/tmp on Unix). OTOH, the SMV file is deleted after solving as it may be huge, depending on the size of the domain.

Currently, the only way to read an SMV file is to reproduce it by yourself, by running Electrod by hand on the said .elo file (which means you need to install Electrod on your machine). I reckon that one may wish for Electrum to show this file, as is done for ordinary Pardinus/Kodkod code.

On the translation

Having said that, I can give some details on the translation, which is actually quite simple (no fancy stuff). Essentially, Electrod unfolds all quantifications as well as relational construct into an LTL formula to be satisfied. As NuSMV is a model-checker (not a satisfiability solver), it’s a bit more subtle than that as some parts of the formula may have to be negated before solving (this part is explained in footnote 7 in the paper).

In practice the LTL formula isn’t issued bluntly as an LTLSPEC (in NuSMV parlance). We extract non-temporal subformulas and put them in an INIT section, formulas stating an invariant are put in an INVAR section, while formulas specifying transitions are put in a TRANS section. The rest goes in the LTLSPEC section. We prefer using a TRANS section than an ASSIGN one because the former has a laxer syntax (and because the solving algorithm that we use transforms the ASSIGN section in a TRANS one anyway).

So, we do have a transition system, albeit -possibly- a quite nondeterministic one. Now remark that, for Electrum and NuSMV, an instance is a trace of a transition system, not the transition system itself. Ignoring once again dualization, the trace output by SMV gives rise to an instance or a counter-example for Electrum.

Now, how can we get another trace for the same problem? As NuSMV doesn’t have such a feature, it’s only possible if we implement it. This can be done naively by reifying the first trace as an LTL formula and then re-run NuSMV on an updated problem where we explicitly reject the reified first trace (by negating the formula representing the first trace).

Considering that SMV verification is meant to be used when one is quite sure the specification is correct, it shouldn’t yield any counter-example trace. Furthermore, such a verification is likely to be inefficient. For these reasons, we decided not to implement the trace navigation sketched just above: therefore, so-called “scenario exploration” is only implemented when using the bounded solver directly implemented by Pardinus.

3

Hi David,

thanks for the explanation. I will further go into that.

First I tried to inspect an input file for Electrod. In all my examples the message when checking assertions is for example

Solver=NuSMV Steps=1..10 Bitwidth=4 MaxSeq=4 SkolemDepth=4 Symmetry=20 Mode=batch
No translation information available.

Then when I inspect the tmpdir, I find Java files with Pardinus/Kodkod code and XML files with the instances. Can you show me a simple spec where an .elo file is actually generated?

4

Every specification yields such an .elo file in a directory named after:

  • first the Electrum file containing the model,
  • then “Run” or “Check” depending on the type of command,
  • then the name and scope of the command,
  • then the date when the command was iexecuted,
  • then a unique number (in this directory).

So if I have a file foo.als with a check cmd for 3 but 4 X today at 5.30pm, I’ll find the .elo file in a directory (in the tmpdir) whose name starts with foo_Check_cmd_for_3_but_4_X-2021-09-13-17-30-123456 (where 123456 is the said unique number).

EDIT: on Linux, this is the way it works, at least.

5

The printing of the .elo file is done in ElectrodSolver::go and I should find the file in the folder determined by java.io.tmpdir. But this is not the case, so I suspect that the method is not called??

Btw I’m on Mac, but that should make no difference

Can I use the SimpleCLI instead of the SimpleGUI with a tracing of the rep.debug messages in ElectrodSolver?

6

Sorry I don’t know this part of the tool well enough, let’s ping @nmacedo .

7

Hi.

That is indeed where the .elo files should be, in java.io.tmpdir in a directory with the name described by @grayswandyr. I’m also on Mac, just tested it and the files are there.

The only thing that I can think of is that, if you are not on debug mode (Options → Verbosity → Debug), those temporary files are deleted on exit.

8

Hi,

I switched to debug mode, but still no .elo files.

Maybe I use an outdated version of Electrum? I use
Electrum Analyzer 2.1 (forked from Alloy Analyzer 5.1) built 2021-04-21T14:18:04.241Z

9

I just tested with that version on my side and I can see .elo files… Can you see the temporary directories or not even that?

10

Hi,

I’m doing the following steps:

  1. I start electrum with
    exec java -Duser.language=en -Djava.io.tmpdir=tmp/electrum -Xdock:name="Electrum" -Xdock:icon=~/bin/icons/Alloy.icns -jar ~/bin/electrum.jar

  2. I load a simple example of a protocol for mutual exclusion using a binary semaphore:

	enum Sstate{ Zero, One }
	one sig S {
		var val: one Sstate
	}
	
	abstract sig State {}
	one sig N, W, C extends State{}
	
	abstract sig Process {
		var state: one State
	}
	one sig P1, P2 extends Process {}
	
	pred init {
		S.val = One
		P1.state = N
		P2.state = N 
	}
	
	pred step1 [P: Process] {
		(P.state = N) => state' = state ++ P -> W && val' = val
								else state' = state && val' = val
		
	}
	
	pred step2 [P: Process] {
		(P.state = W && S.val = One) => state' = state ++ P -> C && S.val' = Zero
											       else state' = state && val' = val
	}
	 
	pred step3 [P: Process] {
		(P.state = C) => state' = state ++ P -> N && S.val' = One
						    else state' = state && val' = val
	}
	
	fact traces{
		init
		always { 
			one P: Process | step1[P] or step2[P] or step3[P]
		}
	}
	
	
	check Safety {
		always { not (P1.state = C) || not (P2.state = C) }
	}
	
	check WeakLiveness {
		always eventually P1.state = C or
		always eventually P2.state = C
	}
	
	check Fairness {
		always eventually P1.state = C and
		always eventually P2.state = C
	}

  1. I set the option Options>Solver>Electod/NuSMV

  2. I clear the temporary directory
    Temporary directory has been cleared.

  3. I run Check Safety:

Starting the solver...

   Forced to be exact: this/Sstate
Executing "Check Safety"
   ...
   Sig this/P1 == [[P1$0]]
   Sig this/P2 == [[P2$0]]
   Sig ordering/Ord == [[ordering/Ord$0]]
   Generating facts...
   Simplifying the bounds...
   Solver=NuSMV Steps=1..10 Bitwidth=4 MaxSeq=4 SkolemDepth=4 Symmetry=20 Mode=batch
   Generating CNF...
   Generating the solution...
   No translation information available. 125ms.
   No counterexample found. . may be valid. 458ms.

The result is as expected. Saftey is fulfilled.

  1. I inspect the directory where java.io.tmp.dir is set to:

tree executed in ~/tmp/electrum gives

.
├── alloy4tmp40-br
│   ├── binary
│   │   ...
│   │   ├── electrod
│   │   ...
│   ├── models
│   │   ...
│   └── tmp
│       └── 97405
│           └── 0.cnf.java

The .java file ends with

PardinusSolver solver = new PardinusSolver(opt);
System.out.println("Solving...");

No .elo file there.

  1. Sorry about the trouble, may be I’m missing something really obvious??
11

Hi.

Just repeated the steps you described and you’re right! It seems there is an issue with the propagation of the command line options down to the solvers: the .elo files are still being created in the default java.io.tmpdir directory.

Can you check whether that is the case on you side? Mines are at /private/var/folders/....

12

Hi,

yes, I found a file named 00000.elo which was generated at the time I run the safety check. It is not so easy to find the file, but sudo find . -name “*.elo” -print in /private/var/folders does the job.

So I’m going to go a little deeper into electrod. I will run the .elo file in a stand alone installtion of electrod.

Thanks for the help!

13

Hi David,

after trying more with Electrum and inspecting the generated elo file, I would like to clarify my question:

In Alloy, the number of objects under consideration is given by the scope, usually 3. So if I define a graph, for example, it has up to 3 nodes in the models generated by Alloy and I can explore runs of the specification by clicking on “New Config”, “New Path” and so forth. And I can get several execution paths for the same graph, and this for each of the graphs up to 3 nodes.

Now, if I do an unbounded analysis with NuSMV, which of these graphs is used for the analysis? Or is the analysis carried out in NuSMV with all possible symmetrical graphs with up to 3 nodes and an infinite number of steps?

Kind regards
Burkhardt Renz

P.S. Your online book “Formal Software Design with Alloy 6” is very helpful in understanding Alloy 6, the modeling tips in particular are enlightening.

14

Hi Burkhardt,

Indeed, the analysis is carried with up to 3 nodes and an infinite number of steps. The generated SMV file also carries symmetry breaking formulas.

Regarding the book, happy to see it’s useful. We hope to be able to publish it formally once it’s finished, hopefully under an open access license.

best,
david