Alloy function outputs no object

1

Hi there,
I am writing a simple model for relationship between Url, Origin, SameSite.
Then, I am applying a very simple check which should be intuitively true, but the counterexample shows that whereas “samesite” function outputs none, “origin” function outputs an Origin object. How can I make sure that the functions always output the objects with the mandatory fields which are given in Url?


module url

sig Scheme, Port, Path {}
sig Domain, SubDomain {}

sig Origin {
  scheme: Scheme,
  subdomain: lone SubDomain,
  host: Domain,
  port: lone Port
}
sig SameSite {
  scheme: Scheme,
  host: Domain,
  port: lone Port
}

sig Url {
  scheme: Scheme,
  host: Domain,
  subdomain : lone SubDomain,
  port: lone Port,
  path: Path
}


fun origin [u : Url]:Origin{
	{o : Origin | o.scheme = u.scheme and o.subdomain=u.subdomain and o.port = u.port and o.host = u.host }
}

fun samesite [u : Url]: SameSite {
	{o : SameSite | o.scheme = u.scheme and o.port = u.port and o.host = u.host }
}
--this check finds a counterexample
check{
	all u : Url | origin[u].scheme = samesite[u].scheme and origin[u].host = samesite[u].host
} for 1

pred x [u : Url]{
	one o : Origin {
		o = origin[u]
	}
}


fact {
  no disj o1, o2: Origin |
    o1 != o2 and o1.scheme = o2.scheme and o1.host = o2.host and o1.subdomain=o2.subdomain and
    o1.port = o2.port
}

fact {
  no disj o1, o2: SameSite |
    o1 != o2 and o1.scheme = o2.scheme and o1.host = o2.host and
    o1.port = o2.port
}
2

This is to be expected: check tries all possible instances of your model. In particular, an instance where there is no inhabitant of Samesite, one in Url and one in Origin is possible. In that case, samesite is correct in returning the set of Samesites that have some properties in relation to u: Url, namely none.

I don’t know what facts should be imposed to make this different because it depends on what you want to model exactly, how the problem domain is structured…