module analysis/lists

some sig Element {}

abstract sig List {}
one sig EmptyList extends List {}
sig NonEmptyList extends List {
	element: Element,
	rest: List
	}

/*
fact ListGenerator {
	all l: List, e: Element |
		some l': List | l'.rest = l and l'.element = e
	}
*/

pred show () {}
run show expect 0

assert FalseAssertion {
	all l: List | l != l
	}
-- no counterexamples if ListGenerator is not commented out
check FalseAssertion expect 0

pred acyclic (l: List) { no l': l.*rest | l' in l'.^rest }
pred terminated (l: List) { EmptyList in l.*rest }
assert AcyclicIfTerminated {	
	all l: List | terminated (l) => acyclic (l)
	}
check AcyclicIfTerminated

assert TerminatedIfAcylic {	
	all l: List | acyclic (l) => terminated (l)
	}
check TerminatedIfAcylic

pred sublist (short, long: List) {
	short in long.*rest
	}

fun length (l: List): Int { Int #l.*rest }
assert Shorter {	
	all l: List - EmptyList |
		acyclic (l) => some l': l.*rest | int length (l) < int length (l')
	}
check Shorter

assert Shorter' {	
	all l: List - EmptyList |
		acyclic (l) => some l': l.*rest | #l'.*rest < #l.*rest
	}
check Shorter'