Alloy mapping relations

Question

I am pretty much starting to look into alloy for doing some verification. I am trying to practice into making something for represent programming languages simple structure.

An mapping entity has a program and dependency relations

A program has functions

Functions have lines of code

Dependency relations is an entity that maps 2 lines of code in some function in the program between each other

Here is what I tried to do but the output graph shows a line of code that is linked to a dependency tuple but not matched to the function. I need all lines of code to be in a function and they can be in dependencies or not...

abstract sig mapping{}

sig Dependency extends mapping {dep0,dep1: one line}

one sig Program extends mapping{ F: some function, D: some Dependency }

//mapping entity is composed of Dependency pairs 2 lines of code 
//and one program which has functions and dependency pairs

sig function { Line : some line}
//Function is made of line of code

abstract sig line{}

run {}

Answer 1

You should add some facts that will enforce the constraints you have in mind for your model.

For example, to enforce that every line has a corresponding function, you can write something like

fact LinesBelongToFunctions {
  all ln: line | 
    one f: function | 
      ln in f.Line
}

This fact says that for each line ln there exists exactly one function f such that f.Lines contains line ln.