import java.util.*;
import rwth.i2.ltlrv.LTL;

public class IteratorTest {

/*
 *
 */
@LTL("java.util.Collection c, java.util.Iterator i:\n" +
        "G(\n" +
        "   (\n" +
        "       exit(call(* java.util.Collection.iterator()) && target(c))  returning i\n" +
        "   ) -> (\n" +
        "       X(\n" +
        "           G(\n" +
        "               (\n" +
        "                   entry((call(* java.util.Collection+.add*(..))||call(* java.util.Collection+.remove*(..))) && target(c))\n" +
        "               ) -> (\n" +
        "                   G(!(\n" +
        "                       entry(call(* java.util.Iterator.next()) && target(i))\n" +
        "                   ))\n" +
        "               )               \n" +
        "           )\n" +
        "       )\n" +
        "   )\n" +
        ")\n" +
        "")

    public static void main(String[] args) {

		Object someObject = "someObject";
		Object someObject2 = "someObject2";

		System.out.println("Create collection...");
		Collection c = new ArrayList();

		System.out.println("Add objects...");
		c.add(someObject);
		c.add(someObject2);

		Iterator iter = c.iterator();
		System.out.println("Get 1st element via iterator...");
		iter.next();

		//do something with c.next();
		//then...

		//modify c
		System.out.println("Modify collection...");
		c.remove(someObject2);

		//invoke c.next() again - invalid, since c was modified in between
		System.out.println("Try to get 2nd object...");
		iter.next();

	}
}