implement reference refinement needed for redefinition: test case redefinition.cfr.
abstract Component
abstract InPort ->> Signal
abstract OutPort ->> Signal
abstract Signal
abstract Command : Signal
abstract MotorCommand : Command
motorDown : MotorCommand
abstract Request : Signal
stop : Request
abstract Controller : Component
abstract req : InPort -> Request ?
down : Request
WinController : Controller
req : req -> stop
cmd : OutPort -> MotorCommand
and the generated Alloy looks like this (it produces exactly one instance):
open util/integer
pred show {}
run show for 1 but 2 c0_Request, 3 c0_Signal
abstract sig c0_Component
{ r_c0_InPort : set c0_InPort
, r_c0_OutPort : set c0_OutPort }
abstract sig c0_InPort
{ c0_InPort_ref : one c0_Signal }
{ one @r_c0_InPort.this }
abstract sig c0_OutPort
{ c0_OutPort_ref : one c0_Signal }
{ one @r_c0_OutPort.this }
abstract sig c0_Signal
{}
abstract sig c0_Command extends c0_Signal
{}
abstract sig c0_MotorCommand extends c0_Command
{}
one sig c0_motorDown extends c0_MotorCommand
{}
abstract sig c0_Request extends c0_Signal
{}
one sig c0_stop extends c0_Request
{}
abstract sig c0_Controller extends c0_Component
{ r_c0_req : lone c0_req
, r_c0_down : one c0_down }
{ r_c0_req in r_c0_InPort }
abstract sig c0_req extends c0_InPort
{ c0_req_ref : one c0_Request }
{ one @r_c0_req.this
c0_req_ref in c0_InPort_ref }
sig c0_down extends c0_Request
{}
{ one @r_c0_down.this }
one sig c0_WinController extends c0_Controller
{ r_c1_req : one c1_req
, r_c0_cmd : one c0_cmd }
{ r_c1_req in r_c0_req
r_c0_cmd in r_c0_OutPort }
one sig c1_req extends c0_req
{ c1_req_ref : one c0_stop }
{ c1_req_ref in c0_req_ref }
one sig c0_cmd extends c0_OutPort
{ c0_cmd_ref : one c0_MotorCommand }
{ c0_cmd_ref in c0_OutPort_ref }
numberOne -> 1
alice -> "Alice"
likertScaleVal -> 1, 2, 3, 4, 5
// non-zero integer
nonZero -> integer -- 0
abstract Person
abstract Head
likes -> Person ?
Alice : Person
`Head
[ likes = Ella ]
// however, now we can use . as super type expressions
Ella : Person
h : Person.Head
[ no likes ]
// expressions now allowed as reference target
heads -> Person.Head *
friend -> Alice ++ Ella 2
onlyAlice -> Alice ** Person
assert [ Alice in onlyAlice.ref ]
assert [ Ella not in onlyAlice.ref ] // interestingly, Alloy detects that
// it's redundant because types are disjoint!!!
exceptElla -> Person -- Ella
assert [ Alice in exceptElla ]
assert [ Ella not in exceptElla ]
These assertions are proven to hold in Alloy. The generated Alloy is:
open util/integer
pred show {}
one sig c0_numberOne
{ c0_numberOne_ref : one 1 }
one sig c0_alice
{ c0_alice_ref : one 0 }
one sig c0_likertScaleVal
{ c0_likertScaleVal_ref : one (((1 + 2) + 3) + 4) + 5 }
one sig c0_nonZero
{ c0_nonZero_ref : one Int - 0 }
abstract sig c0_Person
{ r_c0_Head : set c0_Head
, r_c0_likes : lone c0_likes }
abstract sig c0_Head
{}
{ one @r_c0_Head.this }
sig c0_likes
{ c0_likes_ref : one c0_Person }
{ one @r_c0_likes.this }
one sig c0_Alice extends c0_Person
{ r_c1_Head : one c1_Head }
{ r_c1_Head in r_c0_Head
(this.(@r_c0_likes.@c0_likes_ref)) = c0_Ella }
one sig c1_Head extends c0_Head
{}
one sig c0_Ella extends c0_Person
{ r_c0_h : one c0_h }
{ no this.@r_c0_likes }
one sig c0_h
{}
sig c0_heads
{ c0_heads_ref : one c0_Head }
fact { all disj x, y : c0_heads | (x.@c0_heads_ref) != (y.@c0_heads_ref) }
fact { 2 <= #c0_friend and #c0_friend <= 2 }
sig c0_friend
{ c0_friend_ref : one c0_Alice + c0_Ella }
fact { all disj x, y : c0_friend | (x.@c0_friend_ref) != (y.@c0_friend_ref) }
one sig c0_onlyAlice
{ c0_onlyAlice_ref : one c0_Alice & c0_Person }
assert assertOnLine_37 { c0_Alice in (c0_onlyAlice.@c0_onlyAlice_ref) }
check assertOnLine_37 for 1 but 2 c0_Person, 2 c0_friend, 2 c0_likes
assert assertOnLine_38 { c0_Ella not in (c0_onlyAlice.@c0_onlyAlice_ref) }
check assertOnLine_38 for 1 but 2 c0_Person, 2 c0_friend, 2 c0_likes
one sig c0_exceptElla
{ c0_exceptElla_ref : one c0_Person - c0_Ella }
assert assertOnLine_43 { c0_Alice in (c0_exceptElla.@c0_exceptElla_ref) }
check assertOnLine_43 for 1 but 2 c0_Person, 2 c0_friend, 2 c0_likes
assert assertOnLine_44 { c0_Ella not in (c0_exceptElla.@c0_exceptElla_ref) }
check assertOnLine_44 for 1 but 2 c0_Person, 2 c0_friend, 2 c0_likes
--noalloyruncommandoptionand the generated Alloy looks like this (it produces exactly one instance):
Also, the following advanced test case now works in Alloy: mergeExpAndSetExpAlloy.cfr.
These assertions are proven to hold in Alloy. The generated Alloy is: