Using String Alloy

0
votes

I have an Alloy module

module WorkPlace

sig String{}

sig person{}

sig Employee extends person{

name :String, boss: Employee,worker: set Employee}

sig Employee1 extends person{

name :String, boss: Employee,worker: set Employee}


fact Employee{

all e1:Employee, e2:Employee| (e1.name = e2 && e2.name = e1) =>e1 = e2}

run{}

when i triad to run this mode it give me this massage : "Syntax error at line 2 column 5: There are 3 possible tokens that can appear here: NAME seq this "

I don't know what its mean?

2\ If I have 2 Alloy models ,each model has same element i.e mode1/name, model2/name. how can I create a fact or pred which can say mode1/name = model2/name?

regards

1
alloy
"String" is a reserved word. Use "string" instead (or, better, "Name"). - user1513683

1 Answers

1
votes

  1. As user1513683 already answered:

    "String" is a reserved word. Use "string" instead (or, better, "Name")

  2. You can open an existing module from another module, and then in that module you can use all sigs/relations present in any of the two modules. For example:

module 1 (file m1.als): 

module m1

sig S1 {}

module 2 (file m2.als):

module m2

open m1

sig S2 {}

run { #S1 = #S2 }