WIP: building "programs" and computing possible states

src/main/java/verify/SatPlayground.java

@@ -6,16 +6,13 @@ import static verify.Literal.var;
 import static verify.SatPlayground.State.A;
 import static verify.SatPlayground.State.B;
 import static verify.SatPlayground.State.C;
-import static verify.SatPlayground.State.D;
-import static verify.SatPlayground.State.E;
 
+import java.util.ArrayList;
 import java.util.Arrays;
-import java.util.List;
 import java.util.stream.Collectors;
 
 import org.sat4j.minisat.SolverFactory;
 import org.sat4j.specs.ContradictionException;
-import org.sat4j.specs.IProblem;
 import org.sat4j.specs.ISolver;
 import org.sat4j.specs.TimeoutException;
 import org.sat4j.tools.ModelIterator;
@@ -64,93 +61,246 @@ public class SatPlayground
 		}
 	}
 
-	static class Program
-	{
-		public Program then( final Program p )
+
+	public interface Constraint
 	{
-			return new Program();
+		public void add( final ISolver solver, final int t ) throws ContradictionException;
 	}
 
-		public void verify( final State a, final State b, final State c )
+	public static class HoldStateConstraint implements Constraint
 	{
-			// TODO Auto-generated method stub
+		private final State state;
 
-		}
-	}
+		private final int from_t;
 
-	public static Program getValue( final Object destination )
+		public HoldStateConstraint( final State state, final int from_t )
 		{
-		return new Program();
+			this.state = state;
+			this.from_t = from_t;
 		}
 
-	public static Program synchronize()
+		@Override
+		public void add( final ISolver solver, final int t ) throws ContradictionException
 		{
-		return new Program();
+			assert ( t > from_t );
+			solver.addClause( map.clause(
+					not( var( state, from_t ) ),
+					var( state, t ) ) );
+		}
 	}
 
-	public static Program ifelse( final List< State > condition, final Program pTrue, final Program pFalse )
+	static class ProblemState
 	{
-		return new Program();
-	}
+		ArrayList< Constraint > constraints = new ArrayList<>();
+
+		ISolver solver = SolverFactory.newDefault();
 
-	public static Program assertStates( final State... states )
+		void applyConstraints( final int t ) throws ContradictionException
 		{
-		return new Program();
+			for ( final Constraint constraint : constraints )
+				constraint.add( solver, t );
+
+			addDefaultConstraints( solver, t );
+		}
 	}
 
-	public static void main( final String[] args ) throws ContradictionException, TimeoutException
+	static abstract class Program
 	{
-		final Literal p_A0 = var( A, 0 );
-		final Literal p_B0 = var( B, 0 );
-		final Literal p_C0 = var( C, 0 );
+		protected Program child = null;
 
+		protected Program parent = null;
 
-		final String v = "v";
-		final Program p =
-				getValue( v ).then(
-				synchronize() ).then(
-				ifelse(
-					Arrays.asList( B ),
-					assertStates( B ),
-					assertStates( A, C, D, E ) ) );
-
-		p.verify( A, B, C );
-
-		final ISolver solver = SolverFactory.newDefault();
-//		solver.addClause( new VecInt( new int[] {  1     } ) );
-//		solver.addClause( new VecInt( new int[] { -1,  2 } ) );
-//		solver.addClause( new VecInt( new int[] { -2, -3 } ) );
-//		solver.addClause( new VecInt( new int[] {  3,  4,  5 } ) );
+		protected int t = 0;
 
-//		solver.addClause( map.clause( var( A, 0 ) ) );
-//		solver.addClause( map.clause( not( var( A, 0 ) ), var( B, 0 ) ) );
-//		solver.addClause( map.clause( not( var( B, 0 ) ), not( var( C, 0 ) ) ) );
-//		solver.addClause( map.clause( var( C, 0 ), var( D, 0 ), var( E, 0 ) ) );
+		protected String name;
+
+		public Program( final String name )
+		{
+			this.name = name;
+		}
+
+		public Program then( final Program p )
+		{
+			child = p;
+			p.parent = this;
+			return p;
+		}
 
-		addDefaultConstraints( solver, 0 );
-		addDefaultConstraints( solver, 1 );
+		protected void init()
+		{
+			t = ( parent == null )
+					? 0
+					: ( parent.t + 1 );
+			if ( child != null )
+				child.init();
+		}
 
-		final IProblem problem = solver;
-		final boolean satisfiable = problem.isSatisfiable();
-		System.out.println( satisfiable );
+		protected abstract void modifyState( final ProblemState state ) throws ContradictionException;
 
-		final ModelIterator mi = new ModelIterator( solver );
+		// recursively called by children
+		public ProblemState getState() throws ContradictionException
+		{
+			final ProblemState state = ( parent == null )
+					? new ProblemState()
+					: parent.getState();
+			modifyState( state );
+			return state;
+		}
+
+		protected void printPossibleStates()
+		{
+			final State[] ss = State.values();
+			final ArrayList< State > possible = new ArrayList<>();
+			for ( final State s : ss )
+			{
+				try
+				{
+					final ProblemState state = getState();
+					state.solver.addClause( map.clause( var( s, t ) ) );
+					if ( state.solver.isSatisfiable() )
+					{
+						possible.add( s );
+					}
+				}
+				catch ( final ContradictionException e )
+				{}
+				catch ( final TimeoutException e )
+				{
+					e.printStackTrace();
+				}
+			}
+			System.out.println( "(" + t + ") " + name + " : " + possible );
+		}
+
+		protected void printPossibleTraces()
+		{
 			boolean unsat = true;
+			try
+			{
+				final ProblemState state = getState();
+				final ModelIterator mi = new ModelIterator( state.solver );
 				while ( mi.isSatisfiable() )
 				{
 					unsat = false;
 					final int[] model = mi.model();
 					System.out.println( map.model( model ) );
 				}
+			}
+			catch ( final ContradictionException e )
+			{}
+			catch ( final TimeoutException e )
+			{
+				e.printStackTrace();
+			}
+			if ( unsat )
+				System.out.println( "no possible trace" );
+		}
 
+		public void recursivelyPrintPossibleStates()
+		{
+			init();
+			printPossibleStates();
+			if ( child != null )
+				child.recursivelyPrintPossibleStates();
+		}
+	}
 
-		if ( false )
+	static class Init extends Program
+	{
+		public Init( final String name )
 		{
-			System.out.println( var( A, 1 ) );
-			System.out.println( var( B, 0 ) );
-			System.out.println( var( C, 2 ) );
-			System.out.println( var( D, 3 ) );
-			System.out.println( var( E, 1 ) );
+			super( name );
 		}
+
+		@Override
+		protected void modifyState( final ProblemState state ) throws ContradictionException
+		{
+			state.solver.addClause( map.clause( var( A, 0 ), var( B, 0 ), var( C, 0 ) ) );
+			state.applyConstraints( t );
+		}
+	}
+
+	static class GetValue extends Program
+	{
+		private final Object ref;
+
+		public GetValue( final Object ref, final String name )
+		{
+			super( name );
+			this.ref = ref;
+		}
+
+		@Override
+		protected void modifyState( final ProblemState state ) throws ContradictionException
+		{
+			state.constraints.add( new HoldStateConstraint( B, t ) );
+			state.applyConstraints( t );
+		}
+	}
+
+	static class Lock extends Program
+	{
+		public Lock( final String name )
+		{
+			super( name );
+		}
+
+		@Override
+		protected void modifyState( final ProblemState state ) throws ContradictionException
+		{
+			state.constraints.add( new HoldStateConstraint( A, t ) );
+			state.applyConstraints( t );
+		}
+	}
+
+	static class Branch extends Program
+	{
+		public Branch( final String name )
+		{
+			super( name );
+		}
+
+		@Override
+		protected void modifyState( final ProblemState state ) throws ContradictionException
+		{
+			// TODO Auto-generated method stub
+
+		}
+	}
+
+
+	public static void main( final String[] args ) throws ContradictionException, TimeoutException
+	{
+		final String v = "v";
+		final Program p = new Init(  "entry = computeIfAbsent(); " );
+		p.then( new GetValue( v,     "v = entry.getValue();      " ) )
+		 .then( new Lock(            "synchronized( entry ) {    " ) );
+
+		p.recursivelyPrintPossibleStates();
+		p.child.child.printPossibleTraces();
+
+
+
+
+
+
+//		final ISolver solver = SolverFactory.newDefault();
+//		solver.addClause( map.clause( var( A, 0 ) ) );
+//		solver.addClause( map.clause( not( var( A, 0 ) ), var( B, 0 ) ) );
+//		solver.addClause( map.clause( not( var( B, 0 ) ), not( var( C, 0 ) ) ) );
+//		solver.addClause( map.clause( var( C, 0 ), var( D, 0 ), var( E, 0 ) ) );
+//		addDefaultConstraints( solver, 0 );
+//		addDefaultConstraints( solver, 1 );
+//		final IProblem problem = solver;
+//		final boolean satisfiable = problem.isSatisfiable();
+//		System.out.println( satisfiable );
+//		final ModelIterator mi = new ModelIterator( solver );
+//		boolean unsat = true;
+//		while ( mi.isSatisfiable() )
+//		{
+//			unsat = false;
+//			final int[] model = mi.model();
+//			System.out.println( map.model( model ) );
+//		}
 	}
 }