Cope and Drag

Logging

Current State 0

Temporal Trace Map

Click on any trace state to view it.

graph LR; A0((0)):::highlight; A0 --> A1; click A0 call stateclick("0"); A1((1)); A1 --> A2; click A1 call stateclick("1"); A2((2)); A2 --> A3; click A2 call stateclick("2"); A3((3)); A3 --> A4; click A3 call stateclick("3"); A4((4)); A4 --> A5; click A4 call stateclick("4"); A5((5)); click A5 call stateclick("5"); A5 --> A5; classDef highlight fill:#f96,stroke:#333,stroke-width:2px;

Fields

Int
-8
-7
-6
-5
-4
-3
-2
-1
0
1
2
3
4
5
6
7

Unlit
Light0
Light1
Light2
Light3
Light4

left
Light0	Light4
Light1	Light3
Light2	Light1
Light3	Light0
Light4	Light2

right
Light0	Light3
Light1	Light2
Light2	Light4
Light3	Light1
Light4	Light0

inst  cnd_generated {
Int = `-8+`-7+`-6+`-5+`-4+`-3+`-2+`-1+`0+`1+`2+`3+`4+`5+`6+`7
Unlit = `Light0+`Light1+`Light2+`Light3+`Light4
no no-field-guard
left = (`Light0->`Light4)+(`Light1->`Light3)+(`Light2->`Light1)+(`Light3->`Light0)+(`Light4->`Light2)
right = (`Light0->`Light3)+(`Light1->`Light2)+(`Light2->`Light4)+(`Light3->`Light1)+(`Light4->`Light0)

}

Constraints

Directives

Edit Datum

<alloy builddate="Thursday, May 15th, 2025">
<instance bitwidth="4" maxseq="-1" command="temporary-name_source_1" filename="/Users/siddharthaprasad/Desktop/copeanddrag/examples/paper-examples/ring-lights/source.frg" version="4.1" prefixLength="6" loop="5" >

<sig label="seq/Int" ID="0" parentID="1" builtin="yes">
</sig>

<sig label="Int" ID="1" parentID="2" builtin="yes">

</sig>

<sig label="univ" ID="2" builtin="yes">
</sig>

<field label="no-field-guard" ID="3" parentID="2">
<types> <type ID="2"/><type ID="2"/> </types>
</field>

<sig label="Light" ID="4" parentID="2">

</sig>

<sig label="Unlit" ID="5" parentID="4">
<atom label="Light0"/><atom label="Light1"/><atom label="Light2"/><atom label="Light3"/><atom label="Light4"/>
</sig>

<sig label="Lit" ID="6" parentID="4">

</sig>

<field label="left" ID="7" parentID="4">
<tuple><atom label="Light0"/><atom label="Light4"/></tuple>
<tuple><atom label="Light1"/><atom label="Light3"/></tuple>
<tuple><atom label="Light2"/><atom label="Light1"/></tuple>
<tuple><atom label="Light3"/><atom label="Light0"/></tuple>
<tuple><atom label="Light4"/><atom label="Light2"/></tuple>
<types><type ID="4"/><type ID="4"/></types>

</field>

<field label="right" ID="8" parentID="4">
<tuple><atom label="Light0"/><atom label="Light3"/></tuple>
<tuple><atom label="Light1"/><atom label="Light2"/></tuple>
<tuple><atom label="Light2"/><atom label="Light4"/></tuple>
<tuple><atom label="Light3"/><atom label="Light1"/></tuple>
<tuple><atom label="Light4"/><atom label="Light0"/></tuple>
<types><type ID="4"/><type ID="4"/></types>

</field>

</instance>
<instance bitwidth="4" maxseq="-1" command="temporary-name_source_1" filename="/Users/siddharthaprasad/Desktop/copeanddrag/examples/paper-examples/ring-lights/source.frg" version="4.1" prefixLength="6" loop="5" >

<sig label="seq/Int" ID="0" parentID="1" builtin="yes">
</sig>

<sig label="Int" ID="1" parentID="2" builtin="yes">

</sig>

<sig label="univ" ID="2" builtin="yes">
</sig>

<field label="no-field-guard" ID="3" parentID="2">
<types> <type ID="2"/><type ID="2"/> </types>
</field>

<sig label="Light" ID="4" parentID="2">

</sig>

<sig label="Unlit" ID="5" parentID="4">
<atom label="Light2"/><atom label="Light4"/>
</sig>

<sig label="Lit" ID="6" parentID="4">
<atom label="Light0"/><atom label="Light1"/><atom label="Light3"/>
</sig>

<field label="left" ID="7" parentID="4">
<tuple><atom label="Light0"/><atom label="Light4"/></tuple>
<tuple><atom label="Light1"/><atom label="Light3"/></tuple>
<tuple><atom label="Light2"/><atom label="Light1"/></tuple>
<tuple><atom label="Light3"/><atom label="Light0"/></tuple>
<tuple><atom label="Light4"/><atom label="Light2"/></tuple>
<types><type ID="4"/><type ID="4"/></types>

</field>

<field label="right" ID="8" parentID="4">
<tuple><atom label="Light0"/><atom label="Light3"/></tuple>
<tuple><atom label="Light1"/><atom label="Light2"/></tuple>
<tuple><atom label="Light2"/><atom label="Light4"/></tuple>
<tuple><atom label="Light3"/><atom label="Light1"/></tuple>
<tuple><atom label="Light4"/><atom label="Light0"/></tuple>
<types><type ID="4"/><type ID="4"/></types>

</field>

</instance>
<instance bitwidth="4" maxseq="-1" command="temporary-name_source_1" filename="/Users/siddharthaprasad/Desktop/copeanddrag/examples/paper-examples/ring-lights/source.frg" version="4.1" prefixLength="6" loop="5" >

<sig label="seq/Int" ID="0" parentID="1" builtin="yes">
</sig>

<sig label="Int" ID="1" parentID="2" builtin="yes">

</sig>

<sig label="univ" ID="2" builtin="yes">
</sig>

<field label="no-field-guard" ID="3" parentID="2">
<types> <type ID="2"/><type ID="2"/> </types>
</field>

<sig label="Light" ID="4" parentID="2">

</sig>

<sig label="Unlit" ID="5" parentID="4">
<atom label="Light0"/><atom label="Light2"/><atom label="Light3"/>
</sig>

<sig label="Lit" ID="6" parentID="4">
<atom label="Light1"/><atom label="Light4"/>
</sig>

<field label="left" ID="7" parentID="4">
<tuple><atom label="Light0"/><atom label="Light4"/></tuple>
<tuple><atom label="Light1"/><atom label="Light3"/></tuple>
<tuple><atom label="Light2"/><atom label="Light1"/></tuple>
<tuple><atom label="Light3"/><atom label="Light0"/></tuple>
<tuple><atom label="Light4"/><atom label="Light2"/></tuple>
<types><type ID="4"/><type ID="4"/></types>

</field>

<field label="right" ID="8" parentID="4">
<tuple><atom label="Light0"/><atom label="Light3"/></tuple>
<tuple><atom label="Light1"/><atom label="Light2"/></tuple>
<tuple><atom label="Light2"/><atom label="Light4"/></tuple>
<tuple><atom label="Light3"/><atom label="Light1"/></tuple>
<tuple><atom label="Light4"/><atom label="Light0"/></tuple>
<types><type ID="4"/><type ID="4"/></types>

</field>

</instance>
<instance bitwidth="4" maxseq="-1" command="temporary-name_source_1" filename="/Users/siddharthaprasad/Desktop/copeanddrag/examples/paper-examples/ring-lights/source.frg" version="4.1" prefixLength="6" loop="5" >

<sig label="seq/Int" ID="0" parentID="1" builtin="yes">
</sig>

<sig label="Int" ID="1" parentID="2" builtin="yes">

</sig>

<sig label="univ" ID="2" builtin="yes">
</sig>

<field label="no-field-guard" ID="3" parentID="2">
<types> <type ID="2"/><type ID="2"/> </types>
</field>

<sig label="Light" ID="4" parentID="2">

</sig>

<sig label="Unlit" ID="5" parentID="4">
<atom label="Light0"/><atom label="Light1"/><atom label="Light3"/><atom label="Light4"/>
</sig>

<sig label="Lit" ID="6" parentID="4">
<atom label="Light2"/>
</sig>

<field label="left" ID="7" parentID="4">
<tuple><atom label="Light0"/><atom label="Light4"/></tuple>
<tuple><atom label="Light1"/><atom label="Light3"/></tuple>
<tuple><atom label="Light2"/><atom label="Light1"/></tuple>
<tuple><atom label="Light3"/><atom label="Light0"/></tuple>
<tuple><atom label="Light4"/><atom label="Light2"/></tuple>
<types><type ID="4"/><type ID="4"/></types>

</field>

<field label="right" ID="8" parentID="4">
<tuple><atom label="Light0"/><atom label="Light3"/></tuple>
<tuple><atom label="Light1"/><atom label="Light2"/></tuple>
<tuple><atom label="Light2"/><atom label="Light4"/></tuple>
<tuple><atom label="Light3"/><atom label="Light1"/></tuple>
<tuple><atom label="Light4"/><atom label="Light0"/></tuple>
<types><type ID="4"/><type ID="4"/></types>

</field>

</instance>
<instance bitwidth="4" maxseq="-1" command="temporary-name_source_1" filename="/Users/siddharthaprasad/Desktop/copeanddrag/examples/paper-examples/ring-lights/source.frg" version="4.1" prefixLength="6" loop="5" >

<sig label="seq/Int" ID="0" parentID="1" builtin="yes">
</sig>

<sig label="Int" ID="1" parentID="2" builtin="yes">

</sig>

<sig label="univ" ID="2" builtin="yes">
</sig>

<field label="no-field-guard" ID="3" parentID="2">
<types> <type ID="2"/><type ID="2"/> </types>
</field>

<sig label="Light" ID="4" parentID="2">

</sig>

<sig label="Unlit" ID="5" parentID="4">
<atom label="Light0"/><atom label="Light2"/><atom label="Light4"/>
</sig>

<sig label="Lit" ID="6" parentID="4">
<atom label="Light1"/><atom label="Light3"/>
</sig>

<field label="left" ID="7" parentID="4">
<tuple><atom label="Light0"/><atom label="Light4"/></tuple>
<tuple><atom label="Light1"/><atom label="Light3"/></tuple>
<tuple><atom label="Light2"/><atom label="Light1"/></tuple>
<tuple><atom label="Light3"/><atom label="Light0"/></tuple>
<tuple><atom label="Light4"/><atom label="Light2"/></tuple>
<types><type ID="4"/><type ID="4"/></types>

</field>

<field label="right" ID="8" parentID="4">
<tuple><atom label="Light0"/><atom label="Light3"/></tuple>
<tuple><atom label="Light1"/><atom label="Light2"/></tuple>
<tuple><atom label="Light2"/><atom label="Light4"/></tuple>
<tuple><atom label="Light3"/><atom label="Light1"/></tuple>
<tuple><atom label="Light4"/><atom label="Light0"/></tuple>
<types><type ID="4"/><type ID="4"/></types>

</field>

</instance>
<instance bitwidth="4" maxseq="-1" command="temporary-name_source_1" filename="/Users/siddharthaprasad/Desktop/copeanddrag/examples/paper-examples/ring-lights/source.frg" version="4.1" prefixLength="6" loop="5" >

<sig label="seq/Int" ID="0" parentID="1" builtin="yes">
</sig>

<sig label="Int" ID="1" parentID="2" builtin="yes">

</sig>

<sig label="univ" ID="2" builtin="yes">
</sig>

<field label="no-field-guard" ID="3" parentID="2">
<types> <type ID="2"/><type ID="2"/> </types>
</field>

<sig label="Light" ID="4" parentID="2">

</sig>

<sig label="Unlit" ID="5" parentID="4">

</sig>

<sig label="Lit" ID="6" parentID="4">
<atom label="Light0"/><atom label="Light1"/><atom label="Light2"/><atom label="Light3"/><atom label="Light4"/>
</sig>

<field label="left" ID="7" parentID="4">
<tuple><atom label="Light0"/><atom label="Light4"/></tuple>
<tuple><atom label="Light1"/><atom label="Light3"/></tuple>
<tuple><atom label="Light2"/><atom label="Light1"/></tuple>
<tuple><atom label="Light3"/><atom label="Light0"/></tuple>
<tuple><atom label="Light4"/><atom label="Light2"/></tuple>
<types><type ID="4"/><type ID="4"/></types>

</field>

<field label="right" ID="8" parentID="4">
<tuple><atom label="Light0"/><atom label="Light3"/></tuple>
<tuple><atom label="Light1"/><atom label="Light2"/></tuple>
<tuple><atom label="Light2"/><atom label="Light4"/></tuple>
<tuple><atom label="Light3"/><atom label="Light1"/></tuple>
<tuple><atom label="Light4"/><atom label="Light0"/></tuple>
<types><type ID="4"/><type ID="4"/></types>

</field>

</instance>

<source filename="/Users/siddharthaprasad/Desktop/copeanddrag/examples/paper-examples/ring-lights/source.frg" content="#lang forge/temporal
&#xA;
&#xA;/*
&#xA;  When using the custom vis script, remember to click &amp;quot;Run&amp;quot; after
&#xA;  asking for a new trace or config! (the script doesn't re-run automatically)
&#xA;*/
&#xA;
&#xA;------------------------
&#xA;-- Puzzle infrastructure
&#xA;------------------------
&#xA;abstract sig Light {
&#xA;  left: one Light,  -- neighbor to left
&#xA;  right: one Light  -- neighbor to right
&#xA;}
&#xA;var sig Lit, Unlit extends Light {}
&#xA;
&#xA;pred ring {
&#xA;  -- Connected
&#xA;  all x1, x2: Light | x2 in x1.^left and x2 in x1.^right
&#xA;  -- Opposites
&#xA;  left = ~right
&#xA;}
&#xA;
&#xA;pred solved {
&#xA;  Lit = Light
&#xA;}
&#xA;pred init {
&#xA;    -- ONE specific init state, so we can sketch how to exclude loopback 
&#xA;    --   to the very beginning
&#xA;    no Lit
&#xA;    Unlit = Light
&#xA;}
&#xA;
&#xA;pred flip[switch: Light] {
&#xA;  -- Flip the switch for &amp;lt;switch&amp;gt;, which also flips the neighbors
&#xA;  Lit' = Lit - {x: switch+switch.left+switch.right | x in Lit}
&#xA;             + {x: switch+switch.left+switch.right | x not in Lit}
&#xA;}
&#xA;
&#xA;// Look for a solution to the puzzle that involves at *least* 5 states (4 transitions)
&#xA;option min_tracelength 5
&#xA;// We need more than 5 states to find a solution
&#xA;option max_tracelength 10 
&#xA;
&#xA;// option verbose 5
&#xA;run {
&#xA;    -- well-formedness constraints
&#xA;    ring
&#xA;    -- start in an initial state
&#xA;    init 
&#xA;
&#xA;    -- transition predicate: either flip a single light, or we're done
&#xA;    always {        
&#xA;        -- Do nothing for a solved board. Otherwise, flip a switch
&#xA;        {            
&#xA;            solved -- guard
&#xA;            Lit = Lit' -- action
&#xA;        } or {
&#xA;            not solved -- guard
&#xA;            one l: Light | flip[l] -- action
&#xA;        }        
&#xA;    }
&#xA;
&#xA;    -- find a trace that leads to a solved state
&#xA;    eventually solved
&#xA;
&#xA;    -- If we wanted, we could exclude some unproductive behavior by adding, e.g.:
&#xA;    -- Loopback can't be to the beginning
&#xA;    --next_state { always { some Lit }}    
&#xA;    
&#xA;} 
&#xA;for exactly 5 Light, 5 Lit, 5 Unlit
&#xA;"></source>
</alloy>