So, I tried to use seq in an Electrum model and it fails to parse because module util/sequniv uses primed names. Will this be fixed? What’s the currently recommended work-around?
I’ve flagged it as a bug. When Electrum is moved to the Alloy 6 code base it is hopefully fixed. Which I hope will happen soon.
I do not know a workaround at the moment 
OK. I’ll live without seq for now.
It’s fixed in the forthcoming release candidate. We’ll soon make an announcement.
My favorite workaround is to avoid using sequences as much as I can 
If you really need them now, you may use the util/sequence module I think.
I also avoid them but that is mostly because they awkward to use. In many of my problems ordering is very important. So how do you solve these type of problems?
Well there’s no magical wand that would work for all such situations.
As you say, sequences (in the seq sense) feel a bit awkward (to me at least) and may be costly in terms of size of the state space.
Therefore I try to put as few constraints as possible on the data that must be ordered. For instance by just declaring the piece of data as a plain field, constrained by a fact that doesn’t impose as much as totally ordered sequences of things. Or by “concretizing” the sequence as two or three fields, which may be deemed enough (depending on the problem at hand) to evaluate whether there are problems in your model (= an abstraction of a problem at hand).
No, module util/sequence[elem] also uses primed names.
So, I’m not using seq in a constraint in my model. What I want to do is have the trace of my model be shown in the visualiser. I’d like to do this as a hook for getting the testers at work interested. My first thought was to do something like this:
abstract sig Command {
,vehicle: one Vehicle
,zone: Zone}
sig UnlockCommanded extends Command{
}{
vehicle.unlockAZone[zone]
}
sig Script{
,futureCommands: seq Command
,pastCommands: seq Command
}
pred Script::step{
!isEmpty[this.futureCommands] =>
this.futureCommands' = rest[this.futureCommands]
and add[this.pastCommands, head[this.futureCommands, this.pastCommands']]
}
If there’s another way to make it so that my testers can see what Electrum thinks the trace looks like all at once the I’d love to learn it.
Yes but, if you really need it, as a workaround, you may copy-paste sequence in a new file and replace all primes by " (which is an accepted symbol in Alloy). Then you just open the new file. You can’t do this with seq as it’s wired in the tool.
1 Like
IIUC, you’d like to say you have a sequence of commands to execute in order, and once a command is executed, you keep it in a list of past commands (is there a reason for this).
As it is, the model does not feature any var field or sig so no mutation may happen, anyway…
Also the add part seems bogus to me, shouldn’t it be this.pastCommands' = (this.pastCommands).insert(0, head[this.futureCommand]))?
Also you’re not saying that nothing happens if the list of future commands is empty. So anything may happen.
But I’m not sure to see what you want to demonstrate? Here, the Visualizer could show commands going from one sequence to the other but is it compelling enough? I’m certainly biased but, to me, the interest of Alloy or Electrum is not to simulate the execution of sequential algorithms: encoding loops is tedious, and the fact that -in Electrum- you only have infinite traces hinders reasoning about normal or abnormal termination. If indeed you want to run sequential algorithms, I would rather use another tool…
In my opinion, Electrum really shines when your model is likely to have unexpected (to you) behaviors, and you expect the Visualizer to show them. Or when you want to check some non trivial property of a concurrent or distributed system. For plain Alloy, the same can be said when you want to assess structural designs, or check some invariants, or do some temporal reasoning that does not fit in the linear-time view enforced by Electrum.
OK, so I did that, and then
sig Script{
,futureCommands: Seq
,pastCommands: Seq
}
pred Script::step{
!isEmpty[this.futureCommands] =>
rest[this.futureCommands, this.futureCommands'] //rest is a pred
and add[this.pastCommands, first[this.futureCommands], this.pastCommands'] // add is a pred, first is a fun
}
which produces this error
Name cannot be resolved; possible incorrect
function/predicate call; perhaps you used ( ) when you
should have used [ ]
This cannot be a correct call to pred sequence/add.
The parameters are
s: {sequence/Seq}
e: {this/Command}
added: {sequence/Seq}
so the arguments cannot be
sequence/inds[s] (type = {sequence/SeqIdx})
Int[1] (type = {Int})
This cannot be a correct call to fun integer/add.
The parameters are
n1: {Int}
n2: {Int}
so the arguments cannot be
sequence/inds[s] (type = {sequence/SeqIdx})
Int[1] (type = {Int})
where sequence\add is
pred add [s: Seq, e: elem, added: Seq] {
added.startsWith[s]
added.seqElems[s.afterLastIdx] = e
#added.inds = #s.inds.add[1]
}
I find this deeply perplexing.
This is an interesting discussion. One of the difficulties for outsiders is to understand the appropriateness of each tool.
In this case, is there a way to export the various stages that we can see in the visualiser, rather than trying to record them in the actual model?
Ok, so, the problem I think Alloy/Electrum might be able to help me with is some folks at work who struggle to reconstruct their understanding of some tricky real-world behaviour every time they have to do something new with it. They in particular struggle to extend their testing to cover new behaviour. The system in question is the remote-control “zonal locking” on light commercial vehicles.
I am not trying to find defects in the real world system, it is what it is. That said, if we did find something surprising it might lead to a recall on a vehicle manufacturer’s most profitable product, so that would be fun. It is a distributed system, but I’m not looking for tricksy computer science properties of it. Again there might be some surprises hidden away and that would be interesting, but it’s not my near-term goal. And I wouldn’t be able to discuss any such in public anyway.
My near term goal is to record the essential complexity of the real world system in a way that can be demonstrated to be correct and that can aid practitioners in their day-to-day work. And one of the biggest difficulties I see is with testing. So, my thought is to model the behaviour of the remote and the vehicle as described in the vehicle users’ manual (and eventually some other channels that will interact with the vehicle security system, but that are proprietary). And I’d like to be able to show testers how that model can generate test cases for them. There’s no “sequential algorithm”, there’s “sequences of things that a user might try to do”, and I’d like the Visualiser to make visible those sequences as well as allowing someone, for example a tester, to step through the effect on the model.
The sequence of commands that I’d like to be able to see would turn into a test script: user commands this, vehicle in fact does that.
As a matter of fact, yes (well almost)!
In the new Electrum Visualizer, once you’re satisfied with a trace, you may export it as Electrum code! Go to File->Export->LTL and copy the code. Paste it in a fresh run command and you’re done. A caveat: there’s an issue with lines in the export that feature Int/..., just delete them and it should be ok.
Apparently, you have at least a namespace issue: add is also defined in module integer (which may be opened implicitly… I’m not sure about that). Try using namespace disambiguation by writing sequence/add (if your module is called sequence).
OK. I’m not fully sure to grasp everything but this may be useful: perhaps you don’t need Script, futureCommands and pastCommands at all. IIUC, at every instant, a command is “executed” or execution is over. So if you have a way to know which command is executed at each step, then a trace will necessarily contain, in particular, the list of commands. Would it be enough? If that is so, I can demonstrate our favorite way to do this in a later post.
Ok, this yak will remain unshaven. Thanks.
Yes, that would be enough. A explanation of how to do that would be most welcome.
Sorry for the delay.
So, with what I know, I would represent commands as events. Events are represented as predicates. Then, using the “reified event” idiom, occurring events will be present in every trace you’ll get. As a matter of fact, they will be the commands you were trying to memorize in the Script sig. You may export the trace to retrieve them in a shape amenable to further processing in the context of testing.
Hope this helps.
1 Like