Open stefjoosten opened 3 months ago
This again seems a case of the Sinterklaas issue. The rule you expect to be violated is:
RULE UniverseExists : "_UNIVERSE"[Module] |- I[Module]
This rule can NEVER be violated.
You might give the following rule a try:
ENFORCE -"_UNIVERSE"[Module] |- "_UNIVERSE"[Module]
The compiler generates the following SQL-fragment for computing the violations:
select distinct t1.src as src, t1.tgt as tgt
from (select "Module" as src, "Module" as tgt
from "Module" where "Module" = '_UNIVERSE') as t1
left join
(select "Module" as src, "Module" as tgt from "Module"
where "Module" is not null) as t2
on (t1.src = t2.src) and (t1.tgt = t2.tgt)
where (t2.src is null) or (t2.tgt is null)
This explains the runtime behavior because t1
will be empty.
An alternative way to write the fact that the universe exists might be:
RULE UniverseExists : "_UNIVERSE"[Module]
@sjcjoosten , would this be a correct rule in your opinion?
The compiler wants it to be the only atom in Module
, because it comes back with the following error message, after I took a second module Foo
in the population:
0.263 /usr/local/project/modules.adl:205:1 error:
0.263 There are 3 violations of RULE "UniverseExists":
0.263 ("Foo", "Foo")
0.263 ("Foo", "_UNIVERSE")
0.263 ("_UNIVERSE", "Foo")
0.263 2024-03-30 10:45:51.621869: [error] ExitFailure 10
I had a call with @stefjoosten . I mentioned the rule
r ; I = I ; r = r
In Ampersand, at runtime we have our population in a database, and we check that population for violations of rules. So if we speak about a violation, we actually say that the content of the database violates that rule.
Any expression may be used as the expression of a rule. So to check that "_UNIVERSE" exists in our population, we need a properly typed expression: "_UNIVERSE"[Module]
. This expression can be used as the formal expression of a rule:
RULE UniverseExists : "_UNIVERSE"[Module]
This must be translated into an SQL expression that checks for violations in the database. It must return nothing if "_UNIVERSE" exists in the concept Module. But what should it return if "_UNIVERSE" is missing??
To find violations of some expression expr
, we look for differences between what we find in the population (the database) and tuples in the expression. In this case, that is
\{ (x,y) | x \in Module, y \in Module, (x,y) \notin ('\_UNIVERSE','\_UNIVERSE') \}
This is exactly what is returned as violations, but is not what you intended.
Maybe we need a new operator for this intention?
Or the rule should be defined something like:
RULE newAttempt : V[Module] ; "_UNIVERSE" ; V[Module]
I have done some more thinking on this issue. The newAttempt
rule above doesn't do the job, for if there aren no modules at all, there is no violation detected, which contradicts with Stef's intention.
If the population is empty, no violations will be reported, because the difference between what we find in the population (the database) and tuples in the expression will be empty. Hence no violations.
Fortunately, the population must never be empty, because ONE[ONE] is there by definition. At least, a proper implementation of Ampersand must guarantee that. If we take this into account, a true way to express Stef's intention will be:
RULE universeExistsDoneProperly : V[ONE*Module]; "_UNIVERSE" ; V[Module*ONE]
Currently, I believe it is possible to remove ONE[ONE]
from the population. That should be fixed by fixing the translation of expression to SQL to let that SQL not inspect the database for it, but merely translate it to
select "ONE" as "ONE";
What happened
I ran the following Ampersand script for the purpose of demonstrating that the rule
UniverseExists
guarantees that the atom_UNIVERSE
of typeModule
always exists.I executed the prototype. To my surprise, I found that I can delete module
_UNIVERSE
in the most straightforward way:https://github.com/AmpersandTarski/Ampersand/assets/275768/2e57e2b8-0529-4563-8ee7-443adb285019
What I expected
I expected that the prototype would not let me delete module
_Universe
. Just to verify, I compiled the script without the population statement. As expected I got a compiler message that noticed the missing module:This confirms my expectation that the back end should not allow me to delete module
_UNIVERSE
.Version of ampersand that was used
I ran the prototype on ampersandtarski/prototype-framework:v1.14, which runs Ampersand-v4.6.2 [51c3de2e65c540ef026925fe8547c991765a5588:refs/tags/v4.6.2] with the following settings: --[no-]backend True --[no-]frontend True --[no-]metamodel False --[no-]terminal False --[no-]time-in-log True --[no-]trim-cellvalues True --build-recipe Prototype --crud-defaults CRUD --frontend-version AngularJS --ignore-invariant-violations False --interfaces False --language Nothing --namespace "" --output-dir "." --proto-dir "/var/www" --sql-bin-tables False --terminal-width Nothing --verbosity debug