package jlo;

import rwth.i2.ltlrv.LTL;

/**
 * FailSafeEnumJLO
 * 
 * @author Eric Bodden
 */
public class FailSafeEnumJLO {

    @LTL("java.util.Vector c, java.util.Enumeration i:     \r\n" + 
            "    G(     \r\n" + 
            "      (\r\n" + 
            "        exit(call(java.util.Enumeration+.new(..)) && args(c))  returning i    \r\n" + 
            "      ) -> (\r\n" + 
            "        X(    \r\n" + 
            "            G(    \r\n" + 
            "                (    \r\n" + 
            "                    entry((call(* java.util.Vector.add*(..))||call(* java.util.Vector.remove*(..))||call(* java.util.Vector.clear())||call(* java.util.Vector.retainAll(..))||call(* java.util.Vector.set*(..))||call(* java.util.Vector.insertElementAt(..))) && target(c))    \r\n" + 
            "                ) -> (\r\n" + 
            "                    G(    \r\n" + 
            "                        !(    \r\n" + 
            "                            entry(call(java.lang.Object java.util.Enumeration.nextElement()) && target(i))    \r\n" + 
            "                        )    \r\n" + 
            "                    )\r\n" + 
            "                )    \r\n" + 
            "            )    \r\n" + 
            "        )    \r\n" + 
            "      )    \r\n" + 
            "    )")
  int someMember;
}