ASA

[Asa Asa]

hello
  I need to resolve the question of the following
   
  "Write an assert statement to check if the linked list is cyclic.and write afact statement to make the list acyclic"
   
   
  ASA
   

       
---------------------------------
You rock. That's why Blockbuster's offering you one month of Blockbuster Total Access, No Cost.

[jasonreich_uk]

--- In alloy-discuss@..., Asa Asa <asa_789@...> wrote:
> "Write an assert statement to check if the linked list is cyclic.and write afact statement to
make the list acyclic"

Hi there,

Lets assume that your list is represented as,
        sig ListItem {
                next : lone ListItem
        }

A list would be cyclical if, for any one of its items, the chain of successors eventually leads
back to itself. We can use transitivity ( the ^ operator ) to inspect the successors. For
example you could use a predicate like,
        pred Cyclic[li : ListItem] { li in li.^next }

You can stop all lists from being cyclical using the fact,
        fact Acyclic { no li : ListItem | Cyclic[li] }
or even,
        fact Acyclic' { no ^next & iden }
I have no idea which is preferable.

Hope that this is helpful (and more importantly, correct),
Jason Reich

[dirge]

// Assert that there is A cycle
assert Cycle{
no a:Cell |  a in a.^next  
}
check Cycle for 2

//Fact to prevent Cycle
fact cycleFact{
no a:Cell |  a in a.^next  
}