Skip to content
Snippets Groups Projects
Commit bc3140c8 authored by Tobias Pietzsch's avatar Tobias Pietzsch
Browse files

WIP: SAT helpers for reasoning about concurrency

parent ef93416f
No related branches found
No related tags found
No related merge requests found
......@@ -53,6 +53,11 @@
<groupId>org.scijava</groupId>
<artifactId>ui-behaviour</artifactId>
</dependency>
<dependency>
<groupId>org.sat4j</groupId>
<artifactId>org.sat4j.core</artifactId>
<version>2.3.1</version>
</dependency>
</dependencies>
<developers>
......
package verify;
import verify.SatPlayground.State;
public class Literal implements Comparable< Literal >
{
protected final State s;
protected final int t;
protected final boolean negated;
public Literal( final State s, final int t )
{
this( s, t, false );
}
public Literal( final State s, final int t, final boolean negated )
{
assert ( t >= 0 );
this.s = s;
this.t = t;
this.negated = negated;
}
public Literal getVariable()
{
return negated ? new Literal( s, t ) : this;
}
public boolean negated()
{
return negated;
}
@Override
public int hashCode()
{
return 31 * ( 31 * s.hashCode() + t ) + Boolean.hashCode( negated );
}
@Override
public boolean equals( final Object obj )
{
if ( ! ( obj instanceof Literal ) )
return false;
final Literal other = ( Literal ) obj;
return ( other.negated == this.negated )
&& ( other.t == this.t )
&& ( other.s == this.s );
}
@Override
public String toString()
{
return ( negated ? "¬": "" ) + "p_" + s + t;
}
@Override
public int compareTo( final Literal o )
{
int c = t - o.t;
if ( c == 0 )
{
c = s.compareTo( o.s );
if ( c == 0 )
{
c = ( negated ? 1 : 0 ) - ( o.negated ? 1 : 0 );
}
}
return c;
}
public static Literal var( final State s, final int t )
{
return new Literal( s, t );
}
public static Literal not( final Literal literal )
{
return new Literal( literal.s, literal.t, !literal.negated );
}
}
\ No newline at end of file
package verify;
import static verify.Literal.not;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.List;
import org.sat4j.core.VecInt;
import gnu.trove.impl.Constants;
import gnu.trove.map.TObjectIntMap;
import gnu.trove.map.hash.TObjectIntHashMap;
public class LiteralIndexBimap
{
private final TObjectIntMap< Literal > varToId;
private final ArrayList< Literal > idToVar;
public LiteralIndexBimap()
{
varToId = new TObjectIntHashMap<>( Constants.DEFAULT_CAPACITY, Constants.DEFAULT_LOAD_FACTOR, 0 );
idToVar = new ArrayList<>();
idToVar.add( null );
}
public synchronized Literal literal( final int i )
{
if ( i == 0 || Math.abs( i ) >= idToVar.size() )
throw new IllegalArgumentException();
return i < 0
? not( idToVar.get( -i ) )
: idToVar.get( i );
}
public synchronized int id( final Literal l )
{
final Literal v = l.negated() ? not( l ) : l;
int i = varToId.get( v );
if ( i == 0 )
{
i = idToVar.size();
idToVar.add( v );
varToId.put( v, i );
}
return l.negated() ? -i : i;
}
public VecInt clause( final Literal... literals )
{
return clause( Arrays.asList( literals ) );
}
public VecInt clause( final List< Literal > literals )
{
final int size = literals.size();
final int[] clause = new int[ size ];
for ( int i = 0; i < size; i++ )
clause[ i ] = id( literals.get( i ) );
return new VecInt( clause );
}
public List< Literal > model( final int[] model )
{
final ArrayList< Literal > list = new ArrayList<>();
for ( int i = 0; i < model.length; i++ )
if ( model[ i ] > 0 )
list.add( literal( model[ i ] ) );
list.sort( null );
return list;
}
}
\ No newline at end of file
package verify;
import static verify.Literal.not;
import static verify.Literal.var;
//import static verify.SatPlayground.State.*;
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.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;
public class SatPlayground
{
public static enum State
{
A,B,C,D,E;
}
public static int[][] defaultTransitions = new int[][] {
{ 1, 1, 1, 1, 1 },
{ 0, 1, 1, 1, 1 },
{ 0, 0, 1, 1, 1 },
{ 0, 0, 0, 1, 1 },
{ 0, 0, 0, 0, 1 },
};
public static final LiteralIndexBimap map = new LiteralIndexBimap();
public static void addDefaultConstraints( final ISolver solver, final int t ) throws ContradictionException
{
final State[] ss = State.values();
solver.addExactly(
map.clause(
Arrays.stream( ss )
.map( s -> var( s, t ) )
.collect( Collectors.toList() ) ),
1 );
if ( t > 0 )
{
for ( int r = 0; r < ss.length; ++r )
{
for ( int c = 0; c < ss.length; ++c )
{
if ( defaultTransitions[ r ][ c ] == 0 )
{
solver.addClause( map.clause(
not( var( ss[ r ], t - 1 ) ),
not( var( ss[ c ], t ) ) ) );
}
}
}
}
}
static class Program
{
public Program then( final Program p )
{
return new Program();
}
public void verify( final State a, final State b, final State c )
{
// TODO Auto-generated method stub
}
}
public static Program getValue( final Object destination )
{
return new Program();
}
public static Program synchronize()
{
return new Program();
}
public static Program ifelse( final List< State > condition, final Program pTrue, final Program pFalse )
{
return new Program();
}
public static Program assertStates( final State... states )
{
return new Program();
}
public static void main( final String[] args ) throws ContradictionException, TimeoutException
{
final Literal p_A0 = var( A, 0 );
final Literal p_B0 = var( B, 0 );
final Literal p_C0 = var( C, 0 );
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 } ) );
// 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 ) );
}
if ( false )
{
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 ) );
}
}
}
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment