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

public class HashSetTest {

/*
 * Formula annotation stating that no collection within a HashSet should be modified.
 */
@LTL("java.util.Collection c, java.util.HashSet s:" +
"G(" +
"	(" +
"		exit(call(* java.util.HashSet+.add(..)) && target(s) && args(c))"+
"	) -> ("+
"		X("+
"			G("+
"				("+
"					entry((call(* java.util.Collection+.add*(..))||call(* java.util.Collection+.remove*(..))||call(* java.util.Collection+.clear())) && target(c))"+
"				) -> ((entry(call(* java.util.HashSet+.remove(..)) && target(s) && args(c))) R ("+
"					!("+
"						entry(call(* java.util.HashSet+.contains(..)) && target(s) && args(c))"+
"					)"+
"				))	"+
"			)"+
"		)"+
"	)"+
")")

    public static void main(String[] args) {

		HashSet inner = new HashSet();
		HashSet outer = new HashSet();
		System.out.println("adding inner to outer");
		outer.add(inner);
		System.out.println("modifying inner");
		inner.add(5);
		//the following call would issue a specification violation through J-LO because "inner"
		//was modified while being in "outer" and then "outer" was queried if it contains "inner"
		System.out.println("Does outer.contain inner? " + outer.contains(inner));

	}
}