Visualiser showing a lot of random objecs

Search

Navigation

User login

Visualiser showing a lot of random objecs

Posted on: Sun, 06/21/2009 - 09:38

BFL

Joined: 2009-03-23

Points: 14

Visualiser showing a lot of random objecs

Hi,

I've been working on a university assignment (my last attempt (http://alloy.mit.edu/community/node/453) failed...) and I'm modelling the amsterdam subway for the assignment.

I need to :

Your specification should formalize statements like the following:
• One can get from station S1 to station S2 without a stopover.
(e.g., from CS to VU).
• Station S is served by line L.
• One can get from S1 to S2 by means of a single stopover at S3.
• One can get from S1 to S2 by means of two stopovers, at S3 and
S4.
• The ends of line L are stations S1 (at the start) and S2 (at the
end).

That shouldn't be too hard, and I'm currently modelling the system:

module metroherkansing



sig Station

{

   line: some Line,

   directReachable : set Station

}



sig Line { stops : set Station}



sig L50,L51,L52,L53,L54 extends Line {}

//sig Centraal, Zuid, Amstel, Sloterdijk extends Stop {}

sig Sloterdijk,Zuid,OverAmstel,Amstel,Centraal extends Station{}



fact setup

{

   Sloterdijk.line = L50

   Zuid.line = L50+L51

   OverAmstel.line =  L50+L51

   Amstel.line = L51+L53+L54

   Centraal.line = L51+L53+L54



}



fact reachableStations

{

   all s : Station |  s.directReachable =s.line.stops - s

}



//force all stops to be in a line

fact stopInLine

{

   all s:Station | some l:Line | s in l.stops

}



// if a stop is in a line, the line also contains that stop

fact StopInLineVV

{



}



pred show{}

run show for 6

At first: am I doing something obviously wrong at the moment? The model will contain about 15 stops on 5 lines.

Furthermore, when running the visualiser on this code, it starts creating "Station", "Line1", "Line2" etc.
I know this is because of the "for 6" part of the show command, is there a way to improve this behaviour? I'd like to see only the Lines and Stations I have defined.

Using this show predicate doesn't work either:



pred showAll (l: Line ) {}



run showAll

Thank you in advance!

Posted on: Sun, 06/21/2009 - 12:27 #1

Felix Chang

Joined: 2008-05-15

Points: 334

Hi:

I or someone else would have to look at your model in detail
to answer your other questions. But regarding the showing of extra objects,
well the semantics of Alloy does not require a "minimum solution".
It just has to give you one solution (when solutions exist).
So if you have a model that permits up to 10 objects to exist,
and your formula specifically mentioned 2 of them, but if the analyzer
found a solution that satisfies all your criteria but has 5 objects in it,
then the analyzer will show this solution.

Trying to minimize a solution (given a specific minimization criteria) can be
very expensive, and Alloy Analyzer does not do solution minimization automatically.

If you want a model that has no more than 2 stations, then you can add that as a constraint.
Like " fact { #Station <= 2 } ", then Alloy Analyzer will be obligated to ensure that.

Sincerely,
Felix Chang
Alloy4 Developer

Posted on: Sun, 06/21/2009 - 12:52 #2

BFL

Joined: 2009-03-23

Points: 14

Solved, switching sig to 'one sig' solved it.

About the model:

Well, I'm trying to express the notion of stations on a line.
After having done so, I need to be able to check whether it is possible to go from station A to station B without stopovers, so there exists a Line in A.lines which is in B.lines.

But now, I need to calculate whether you need 1 or even 2 stopovers to reach station b.
That's a bit harder, and I was wondering whether the structure (not the contents) of my model are fine.