QCHECK/000755 000765 000024 00000000000 12332735543 012755 5ustar00fspedalistaff000000 000000 QCHECK/._.DS_Store000644 000765 000024 00000000122 12332735550 014646 0ustar00fspedalistaff000000 000000 Mac OS X  2 R QCHECK/.DS_Store000644 000765 000024 00000014004 12332735550 014435 0ustar00fspedalistaff000000 000000 Bud1%  @€ @€ @€ @ E%DSDB`€ @€ @€ @QCHECK/aiger-model/000755 000765 000024 00000000000 12332735341 015136 5ustar00fspedalistaff000000 000000 QCHECK/perl-cegar/000755 000765 000024 00000000000 12332735011 014764 5ustar00fspedalistaff000000 000000 QCHECK/perl-cegar/AbstractAigerModel.pm000644 000765 000024 00000022730 12332735011 021022 0ustar00fspedalistaff000000 000000 package AbstractAigerModel; use Cudd; use AigerModel; use parent Model; #use Scalar::Util; =head1 AbstractAigerModel - data structures for a model that is an abstraction of an underlying AigerModel =head1 Synopsis my $model = new AbstractAigerModel(model=>$model,show=>\@litsToShow) =head1 Description This model class, a subclass of L, hides some of the latches of the underlying B class, which is stored in the C property. Hidden latches are treated as inputs in the abstracted model. =head2 Functions =over =cut # An AbstractAigerModel is made by passing a hash with initargs sub new ($$) { my $class = shift; my $initHashPtr = shift; my %initHash = %$initHashPtr; my $groundModel = $initHash{model} || die "Must specify a value for model in initializer for AbstractAigerModel."; my $showPtr = $initHash{show}; my $hidePtr = $initHash{hide}; die "Must specify list of literals to hide or to show." unless $showPtr || $hidePtr; my $self = {}; bless $self, $class; $self->{groundModel} = $groundModel; if ($showPtr) { $self->{shownLits} = $showPtr; my @hidden; foreach my $latch ($groundModel->latch_literals()) { my $found = grep {$_ == $latch} @$showPtr; push @hidden, $latch unless $found; } $self->{hiddenLits} = \@hidden; } elsif ($hidePtr) { $self->{hiddenLits} = $hidePtr; my @shown; foreach my $latch ($groundModel->latch_literals()) { my $found = grep {$_ == $latch} @$hidePtr; push @shown, $latch unless $found; } $self->{shownLits} = \@shown; } foreach my $l (@hidden) { die "Cannot hide a literal that is not a latch value, $l." unless $self->is_latch($l); } foreach my $l ($self->latch_literals()) { die "All latches must be shown or hidden" unless (grep {$_ == $l} @{$self->{hiddenLits}}) || (grep {$_ == $l} @{$self->{shownLits}}); } return $self; } =item add_latch =cut # latches are pairs of literals sub add_latch ($$) { my $self = shift; die "Should never be adding a latch to an AbstractAigerModel, $self"; } =item add_output =cut sub add_output ($) { my $self = shift; die "Should never be adding an output to an AbstractAigerModel, $self"; } =item add_andgate =cut # although it doesn't line up with the latches, # we use literals for all three of the values here. sub add_andgate ($$$) { my $self = shift; die "Should never be adding an and gate to an AbstractAigerModel, $self"; } =item install_var =cut # $model->install_var($literal, $Bdd) sub install_var ($$) { my $self = shift; die "Should never be installing a variable on an AbstractAigerModel, $self"; } =back =head2 Delegated methods =over =item manager $model->manager() Return the CUDD manager object (see L) corresponding to C<$model>. =cut # start of delegated methods... sub manager { my $self = shift; my $groundModel = $self->{groundModel}; return $groundModel->manager(); } =item all_vars =cut sub all_vars { my $self = shift; my $groundModel = $self->{groundModel}; return $groundModel->all_vars(); } # sub inputs { # my $self = shift; # my $groundModel = $self->{groundModel}; # return $groundModel->inputs(); # } =item outputs =cut sub outputs { my $self = shift; my $groundModel = $self->{groundModel}; return $groundModel->outputs(); } =item latches =cut sub latches { my $self = shift; my $groundModel = $self->{groundModel}; return $groundModel->latches(); } =item andGates =cut sub andGates { my $self = shift; my $groundModel = $self->{groundModel}; return $groundModel->andGates(); } =item is_var =cut # FIXME: badly named -- the argument is a *literal*, not an index... sub is_var ($) { my $self = shift; my $literal = shift; my $groundModel = $self->{groundModel}; return $groundModel->is_var($literal); } =item is_negated =cut sub is_negated ($) { my $self = shift; my $index = shift; my $groundModel = $self->{groundModel}; return $groundModel->is_negated($index); } =item var_index =cut # returns a one-based variable index (yuck!) sub var_index ($) { my $self = shift; my $index = shift; my $groundModel = $self->{groundModel}; return $groundModel->var_index($index); } =item decode_literal =cut sub decode_literal ($) { my $self = shift; my $lit = shift; my $groundModel = $self->{groundModel}; return $groundModel->decode_literal($lit); } =item target_state =cut sub target_state { my $self = shift; my $groundModel = $self->{groundModel}; return $groundModel->target_state(); } =item initial_state =cut # all latches are initially zero... sub initial_state { my $self = shift; my $groundModel = $self->{groundModel}; return $groundModel->initial_state(); } sub is_latch ($) { my $self = shift; my $lit = shift; my $groundModel = $self->{groundModel}; die "No ground model for $self" unless $groundModel; return $groundModel->is_latch($lit); } sub latch_literals { my $self = shift; my $groundModel = $self->{groundModel}; die "No ground model for $self" unless $groundModel; return $groundModel->latch_literals(); } # end of delegated methods =item state_vars See . Returns only the I state variables (unhidden latches). See L for a list of all the variables characterizing this state. =cut sub state_vars { my $self = shift; my @vars; foreach my $latch ($self->latches()) { my ($old, $new) = @$latch; push @vars, $self->decode_literal($old) unless $self->is_hidden($old); } return @vars; } sub next_state_vars { my $self = shift; if (! $self->{_nextStateVarsSet}) { $self->initialize(); } my $vars = $self->{_nextStateVars}; return @$vars; } =item is_hidden C<< $model->is_hidden(4) >> Is the argument LITERAL hidden in the model? =cut sub is_hidden ($) { my $self = shift; my $literal = shift; my $found = 0; die "Cannot hide a non-variable literal" unless $self->is_var($literal); foreach my $lit ( @{$self->{hiddenLits}} ) { if ($lit == $literal) { $found = 1; last; } } return $found; } sub initialize { my ( $self ) = @_; # cache the next state variables, # and they need to go in the transition relation... my @vars; my @literals; my $manager = $self->manager; my $transitionRel = $manager->BddOne; foreach my $latch ($self->latches()) { my ($old, $new) = @$latch; if (! $self->is_hidden($old)) { my $literal = $self->decode_literal($new); my $nextvar = $manager->BddVar; # new variable iff literal $transitionRel=$transitionRel->And($nextvar->Or($literal->Not())); $transitionRel=$transitionRel->And($literal->Or($nextvar->Not())); push @vars, $nextvar; push @literals, $literal; } } $self->{_nextStateVars} = \@vars; $self->{_transitionRel} = $transitionRel; $self->{_nextStateVarsSet} = 1; } sub transition_rel { my $self = shift; if (! $self->{_nextStateVarsSet}) { # need to cache the transition relation $self->initialize(); } return $self->{_transitionRel}; } =item $M->inputCube() Returns a cube of variables computed from =C<$M->inputVars>. See the discussion of that method for remarks about the fact that this will return a cube containing not only the true inputs, but also the hidden literals. =cut sub inputCube { my $self = shift; my @inputVars = $self->inputVars; my $manager = $self->manager(); my $cube = $manager->BddOne; foreach my $var (@inputVars) { $cube = $cube * $var; } return $cube; } # some latches are treated as if they are inputs =item inputVars C<< $model->inputVars() >> Returns a list of input variables, which =I not only the ground model's input variables, but also the hidden literals. If you want only the true input variables, use =C<< $model->groundModel->inputVars() >>. =cut sub inputVars { my $self = shift; my $groundModel = $self->{groundModel}; my @inputs = $groundModel->inputVars(); my @latches = $self->latches(); foreach my $latch (@latches) { my ($old, $new) = @$latch; if ($self->is_hidden($old)) { push @inputs, $self->decode_literal($old); } } return @inputs; } =item $model->latchVars() Return a list of the I latch variables (BDDs). =cut sub latchVars { my $self = shift; my @latches = $self->latches(); my @vars; foreach my $latch (@latches) { my ($old, $new) = @$latch; if (! $self->is_hidden($old)) { push @vars, $self->decode_literal($old); } } return @vars; } =item now_vars See L. Returns a list of variables that characterize the current state of the system. Latches + inputs, I inputs that are hidden latches. =cut sub now_vars { my $self = shift; my @now_vars; @now_vars = ($self->inputVars(), $self->latchVars()); return @now_vars; } =item $model->hidden_vars() Returns a list of the variables (BDD nodes) corresponding to literals hidden in C<$model>. Primarily of use as a debugging tool. =cut sub hidden_vars { my $self = shift; my @hidden = @{$self->{hiddenLits}}; my @vars; foreach my $h (@hidden) { push @vars, $self->decode_literal($h); } return @vars; } =item $model->hiddenCube() Returns a cube (BDD) of the literals hidden in C<$model>. Primarily of use as a debugging tool. =cut sub hiddenCube { my $self = shift; my @vars = $self->hidden_vars(); die "No hidden vars for model $self." unless @vars; my $bdd = $vars[0]->One; foreach my $var (@vars) { $bdd = $bdd * $var; } return $bdd; } =back =cut 1; QCHECK/perl-cegar/adder.pl000755 000765 000024 00000000412 12332735011 016400 0ustar00fspedalistaff000000 000000 #! /usr/bin/env perl use Cudd; my $manager = new Cudd; my $x0 = $manager->BddVar; my $x1 = $manager->BddVar; my $and1 = $x0->And($x1->Not); my $and2 = $x1->And($x0->Not); my $sum = $and1->Or($and2); my $carry = $x0->And($x1); $sum->Print(2,2); $carry->Print(2,2); QCHECK/perl-cegar/aiger-cegar-test.pl000755 000765 000024 00000003110 12332735011 020442 0ustar00fspedalistaff000000 000000 #! /usr/bin/env perl # Test reading and solving models formulated using AIGER use FindBin; use lib ( $FindBin::RealBin ); use Aiger; use AigerModel; use Cudd; use ModelChecker; use warnings; use Carp; use strict; use Getopt::Long; our $verbose = 1; our $help = 0; # opposite of interactive our $programmatic = 0; $SIG{ __DIE__ } = sub { Carp::confess( @_ ) }; { my $result = GetOptions("verbose" => \$verbose, "help" => \$help, "usage" => \$help, "programmatic" => \$programmatic ); die "Error processing command line arguments" unless $result; } sub usage () { print "$0 [--verbose|-v] [--help] [--usage] [--programmatic] \n"; print "\n\tPerform CEGAR model checking on as configured by the\n"; print "command-line options.\n"; print "\tIf --programmatic is passed, the model-checker will use an external solver\n"; print "to handle its ILPs. This requires some minor change in behavior.\n"; } print STDERR "Model: $ARGV[0]\n" if $verbose; my $model = Aiger::read_aig_file($ARGV[0]); # print "Model inputs: "; # print $model->inputs; # print "\n"; # print "Model outputs: "; # print $model->outputs; # print "\n"; # print "Model latches: "; # print $model->latches; # print "\n"; # print "Model and-gates: "; # print $model->andGates; # print "\n"; #exit 0; print "Done reading file and building model.\n" if $verbose; ModelChecker::verbose($verbose); if ($programmatic) { ModelChecker::interactive(0); } ModelChecker::cegar_model_check($model); QCHECK/perl-cegar/aiger-cegar-test.pl~000755 000765 000024 00000001217 12332735011 020646 0ustar00fspedalistaff000000 000000 #! /usr/bin/env perl # Test reading and solving models formulated using AIGER use Aiger; use AigerModel; use Cudd; use ModelChecker; use strict; use warnings; use Carp; $SIG{ __DIE__ } = sub { Carp::confess( @_ ) }; print "$ARGV[0]\n"; my $model = Aiger::read_aig_file($ARGV[0]); # print "Model inputs: "; # print $model->inputs; # print "\n"; # print "Model outputs: "; # print $model->outputs; # print "\n"; # print "Model latches: "; # print $model->latches; # print "\n"; # print "Model and-gates: "; # print $model->andGates; # print "\n"; #exit 0; print "Done reading file and building model.\n"; ModelChecker::cegar_model_check($model); QCHECK/perl-cegar/aiger-test.pl000755 000765 000024 00000001270 12332735011 017370 0ustar00fspedalistaff000000 000000 #! /usr/bin/env perl # Test reading and solving models formulated using AIGER use FindBin; use lib ( $FindBin::RealBin ); use Aiger; use AigerModel; use Cudd; use ModelChecker; use strict; use warnings; use Carp; #$SIG{ __DIE__ } = sub { Carp::confess( @_ ) }; print "$ARGV[0]\n"; my $model = Aiger::read_aig_file($ARGV[0]); # print "Model inputs: "; # print $model->inputs; # print "\n"; # print "Model outputs: "; # print $model->outputs; # print "\n"; # print "Model latches: "; # print $model->latches; # print "\n"; # print "Model and-gates: "; # print $model->andGates; # print "\n"; #exit 0; print "Done reading file and building model.\n"; ModelChecker::model_check($model); QCHECK/perl-cegar/Aiger.pm000644 000765 000024 00000006433 12332735011 016357 0ustar00fspedalistaff000000 000000 package Aiger; require Exporter; @ISA = qw(Exporter); @EXPORT_OK = qw(read_aig_file); use strict; use warnings; use AigerModel; my $verbose = 1; sub read_aig_file ($) { my $filename = shift; my ($M, $I, $L, $O, $A); die "Unable to open file $filename" unless -e $filename; open FILE, "< $filename" || die "Can't open file $filename"; { # read and process header line my $header = ; chomp $header; my @fields = split / /, $header; my $key; ($key, $M, $I, $L, $O, $A) = @fields; die "read_aig_file does not handle ASCII format AAG files. Please use aigtoaig to translate to AIG." if ($key eq "aag"); die "Not an AIG file: $key" unless ($key eq "aig"); if ($#fields == 9) { die "read_aig_file does not handle 1.9 format AIG files."; } elsif ($#fields != 5) { die "not a recognized AIG file header."; } } # end of reading header line my $model = new AigerModel($M, $I, $L, $O, $A); print STDERR "Made new Aiger model with $I inputs, $L latches, $O outputs, and $A and gates.\n"; print STDERR "Reading $L latches.\n" if $verbose; for (my $i = 0, my $j = $I + 1; $i < $L; $i++, $j++) { # $j is 1/2 the literal corresponding to the $ith latch. # literals are 2 * (number of inputs + 1), so $j = $I + 1 # + 1 because 0, 1 are reserved for F, T my $line = ; chomp $line; my @fields = split / /, $line; die "Wrong number of fields $#fields for latch line." unless $#fields == 0; my ($nextIndex) = @fields; $model->add_latch(2 * $j, $nextIndex); } print STDERR "Reading $O outputs.\n" if $verbose; for (my $i = 0; $i < $O; $i++) { my $line = ; chomp $line; my @fields = split / /, $line; die "Wrong number of fields $#fields for output line." unless $#fields == 0; my $lit = $fields[0]; $model->add_output($lit); } binmode(FILE); print STDERR "Reading $A and gates.\n" if $verbose; for (my $i = 0, my $j = $I + $L; $i < $A; $i++, $j++) { my $delta0 = decode(\*FILE); my $delta1 = decode(\*FILE); my $lhs = ($j + 1) * 2; # literal value for LHS -- the index + 1 for one-based, doubled my $rhs0 = $lhs - $delta0; my $rhs1 = $rhs0 - $delta1; $model->add_andgate($lhs, $rhs0, $rhs1); } close FILE; return $model; } sub getnoneofch ($) { my $fh =shift; my $ch = getc($fh); if (! defined($ch)) { die "unexpected EOF"; } return ord($ch); } sub decode ($) { my $file = shift; my $x = 0; my $i = 0; my $ch; while ( ($ch = getnoneofch($file)) & 0x80) { $x |= ($ch & 0x7f) << (7 * $i++ ); } return $x | ($ch << (7 * $i)); } =head1 Aiger - reader for an AIGER format model =head1 SYNOPSIS use Aiger; $model = Aiger::read_aig_file($filename); =head1 DESCRIPTION This module provides a function for reading an AIGER binary mode file (an .aig file), and translate it into an L data structure, which it returns. If you have an AIGER ASCII format file, you can use the C tool to translate it to a binary format file before loading. =head1 DEPENDENCIES L =head1 AUTHOR Robert P. Goldman =head1 LICENSE AND COPYRIGHT Copyright (c) 2013 Robert P. Goldman ($model,show=>\@litsToShow) =head1 Description This model class, a subclass of L, =head2 Functions =over =cut sub new ($$$$$) { my $class = shift; my ($M, $I, $L, $O, $A) = @_; my @allvars; my @inputVars; my $self = $class->SUPER::new; bless $self, $class; die "Currently only handle reachability models with a single output variable" unless $O == 1; # Make variables for all of the inputs and the latches for (my $i = 0; $i < $I; $i++) { my $var = $self->manager->BddVar; push @allvars, $var; push @inputVars, $var; } for (my $i = $I; $i < $I + $L; $i++) { push @allvars, $self->manager->BddVar; }; $self->{_allvars} = \@allvars; $self->{inputCount} = $I; $self->{outputCount} = $O; $self->{latchCount} = $L; $self->{_inputVars} = \@inputVars; $self->{_outputs} = []; # list of output LITERALS $self->{_latches} = []; # list of pairs of LITERALS # later use these for memoizing # $self->{_stateVars} = []; $self->{_nextStateVars} = []; $self->{_nextStateVarsSet} = 0; return $self; } # latches are pairs of literals where the first is the literal # corresponding to the latch itself (this will be a variable), # and the second is a literal which should be evaluated to # set the value of the latch in the next state. sub add_latch ($$) { my ($self, $thisStateLiteral, $nextStateLiteral) = @_; my $latch = [$thisStateLiteral, $nextStateLiteral]; push @{$self->{_latches}}, $latch; return; } =item $self->now_vars() The now_vars of the model are the set of all the vars (which does I include the next state variables, for an odd implementation reason), except the latch variables. This means that when we use this to existentially quantify away the variables from the current state, in computing the image under the transition relation, we will also quantify away the inputs. =cut sub now_vars { my $self = shift; my @allvars = @{$self->{_allvars}}; my $lim = $self->{inputCount}+$self->{latchCount} - 1; return @allvars[0..$lim]; } # The outputs are LITERALS. sub add_output ($) { my $self = shift; my $literal = shift; push @{$self->{_outputs}}, $literal; return; } # although it doesn't line up with the latches, # we use literals for all three of the values here. sub add_andgate ($$$) { my ($self, $lhs, $rhs0, $rhs1) = @_; # print "$lhs $rhs0 $rhs1\n"; die "$lhs is not a positive literal" if $self->is_negated($lhs); my $rhs0Bdd = $self->decode_literal($rhs0); die "Error: $rhs0 literal not yet defined." unless $rhs0Bdd->isa("Cudd::BDD"); my $rhs1Bdd = $self->decode_literal($rhs1); die "Error: $rhs1 literal not yet defined." unless $rhs1Bdd->isa("Cudd::BDD"); $self->install_var($lhs, $rhs0Bdd->And($rhs1Bdd)); return; } # returns a list of input *variables* sub inputVars { my $self = shift; my $inputs = $self->{_inputVars}; return @$inputs; } sub latchVars { my $self = shift; my @latches = $self->latches(); my @vars; foreach my $latch (@latches) { my ($old, $new) = @$latch; push @vars, $self->decode_literal($old); } return @vars; } sub inputCube { my $self = shift; my @inputVars = $self->inputVars; my $manager = $self->manager(); my $cube = $manager->BddOne; foreach my $var (@inputVars) { $cube = $cube * $var; } return $cube; } sub next_state_cube { my $self = shift; my @nsVars = $self->next_state_vars(); my $manager = $self->manager(); my $cube = $manager->BddOne; foreach my $var (@nsVars) { $cube = $cube * $var; } return $cube; } sub outputs { my $self = shift; my $outputs = $self->{_outputs}; return @$outputs; } # Returns a list of literal pairs. The first element is the literal # corresponding to the latch's value in this state. The second element is the # literal that specifies the next state value of the latch sub latches { my $self = shift; my $latches = $self->{_latches}; return @$latches; } sub latch_literals { my $self = shift; my @latches = $self->latches(); my @r; foreach my $l (@latches) { my ($ll, $nl) = @$l; push @r, $ll; } return @r; } sub andGates { my $self = shift; my $andgates = $self->{_andgates}; return @$andgates; } sub state_vars { my ( $self ) = @_; return $self->latchVars(); } sub initialize { my ( $self ) = @_; # cache the next state variables, # and they need to go in the transition relation... my @vars; my $manager = $self->manager; my $transitionRel = $manager->BddOne; foreach my $latch ($self->latches()) { my ($old, $new) = @$latch; my $literal = $self->decode_literal($new); my $oldvar = $self->decode_literal($old); my $nextvar = $oldvar->NewAdjVar(); # new variable iff literal # FIXME: using ITE might be more efficient here... $transitionRel=$transitionRel * ($nextvar + $literal->Not()); $transitionRel=$transitionRel * ($literal + $nextvar->Not()); push @vars, $nextvar; } # foreach my $lit ($self->outputs()) { # my $bdd = $self->decode_literal($lit); # die "Translation of output $lit is not a BDD" unless $self->is_bdd($bdd); # $transitionRel = $transitionRel * $bdd; # } $self->{_nextStateVars} = \@vars; $self->{_transitionRel} = $transitionRel; $self->{_nextStateVarsSet} = 1; } sub next_state_vars { my ( $self ) = @_; if (! $self->{_nextStateVarsSet}) { $self->initialize(); } my $vars = $self->{_nextStateVars}; return @$vars; } sub is_var ($) { my $self = shift; my $index = shift; my $is_var = ( $index > 1 ) && (( $index % 2 ) == 0); return $is_var; } # does the argument literal represent a latch? # FIXME: test this sub is_latch ($) { my $self = shift; my $lit = shift; my $I = $self->{inputCount}; my $L = $self->{latchCount}; return $self->is_var($lit) && # one-based origin... ( $lit > $I * 2 ) && ( $lit <= ($I + $L) * 2); } sub is_negated ($) { my $self = shift; my $literal = shift; return ($literal % 2); } # returns a one-based variable index (yuck!) sub var_index ($) { my $self = shift; my $index = shift; return int ($index / 2); } sub set_state_vars { my($self, @state_vars) = @_; die "Cannot set state vars on an AigerModel."; } sub set_next_state_vars { my($self, @next_state_vars) = @_; die "Cannot set next state vars on an AigerModel."; } sub var_lookup ($) { my $self = shift; my $index = shift; $index--; # AIGER indices are 1-based, not zero-based die "Undefined index" unless ($index || $index == 0); my @allvars = @{$self->{_allvars}}; die "Undefined variable at index $index" if $index > $#allvars; my $var = $allvars[$index]; die "No variable at position $index" unless $var->isa(Cudd::BDD); return $var; } # $model->install_var($literal, $Bdd) sub install_var ($$) { my $self = shift; my $lit = shift; my $val = shift; my $index = $self->var_index($lit); die "Trying to set a negated variable: $lit\n" if $self->is_negated($lit); $index--; # AIGER indices are 1-based, not zero-based ${$self->{_allvars}}[$index] = $val; return; } sub decode_literal ($) { my ($self, $literal) = @_; my $manager = $self->manager(); if ( $literal == 0 ) { return $manager->BddOne->Not; } elsif ( $literal == 1 ) { return $manager->BddOne; } else { my $varindex = $self->var_index($literal); my $negated = $self->is_negated($literal); my $var = $self->var_lookup($varindex); if ( $negated ) { return $var->Not(); } else { return $var; } } } sub transition_rel { my $self = shift; if (! $self->{_nextStateVarsSet}) { # need to cache the transition relation $self->initialize(); } return $self->{_transitionRel}; } # The target state is the output being true. We look # up the literal and decode it. sub target_state { my $self = shift; my @outputs = $self->outputs(); my $count = $#outputs + 1; die "Can only handle single-output models, but this model has $count" unless $#outputs == 0; my $literal = $outputs[0]; # { # my $var = $self->decode_literal($literal); # print "Output literal is $literal, bddVar = $var"; # } return $self->decode_literal($literal); } # all latches are initially zero... sub initial_state { my $self = shift; my $state = $self->manager->BddOne; foreach my $latch ($self->latches()) { my ($literal, $next) = @$latch; my $var = $self->decode_literal($literal); my $negation = $var->Not(); $state = $state * $negation; } return $state; } sub init_latches_to_show { my $self = shift; my @showMe; my @outputs = $self->outputs(); my $supp = $self->manager()->BddOne; # compute a cube of the support of all of the # outputs (for now, only one). foreach my $output (@outputs) { my $outvar = $self->decode_literal($output); $supp = $supp * $outvar->Support(); } foreach my $l ($self->latch_literals()) { my $v = $self->decode_literal($l); if ($supp->LiteralSetIntersection($v) == $v) { push @showMe, $l; } } return @showMe; } sub latchVars { my $self = shift; my @latches = $self->latches(); my @vars; foreach my $latch (@latches) { my ($old, $new) = @$latch; push @vars, $self->decode_literal($old); } return @vars; } =back =cut 1; QCHECK/perl-cegar/cegar-solver-loop.pl000755 000765 000024 00000005461 12332735011 020672 0ustar00fspedalistaff000000 000000 #!/usr/bin/env perl # This is the master command: wraps around the CEGAR model-checker and the # external ILP solver. See "cegar-solver-loop -u" for usage instructions. # use FindBin; use lib ( $FindBin::RealBin ); use IO::File; use POSIX qw(tmpnam); #use Expect; use IPC::Open2; use warnings; use Carp; use strict; use Getopt::Long; # give me a backtrace $SIG{ __DIE__ } = sub { Carp::confess( @_ ) }; our $model; our $solver; our $help = 0; # FIXME: later turn this to 0 our $verbose = 1; # process command-line options { my $result = GetOptions("model=s" => \$model, "solver=s" => \$solver, "verbose" => \$verbose, "help" => \$help, "usage" => \$help ); die "Error processing arguments" unless $result; } # sanity checking if ($help) { usage(); exit 0; } if (!$model) { print STDERR "Must specify model to process."; usage(); exit 1; } if (!$solver) { print STDERR "Must specify solver to handle ILPs."; usage(); #exit 1; } my $command; { my @args; if ($verbose) { push @args, "--verbose"; } # tell CEGAR loop to talk to an external program, not a user. push @args, "--programmatic"; push @args, $model; $command = join(" ",("aiger-cegar-test",@args)); } print "Starting:\n\t $command\n"; my $pid = open2(*README, *WRITEME, $command); while () { print STDERR "Read: $_"; if (m|----------------------------------------|) { print STDERR "Found start of ILP, invoking ilp_callback\n"; ilp_callback(); } } close(README); close(WRITEME); waitpid($pid, 0); exit 0; sub usage { print "$0 --model --solver \n"; print "\tPerform CEGAR model checking on , invoking the \n"; print "\tto solve any ILPs that arise in the process.\n"; } sub ilp_callback { # we have just read the top line of hyphens # read all of the rows my $ilp = ""; my $tmpfile; my $done = 0; while (!$done && ($_ = )) { if (m|----------------------------------------|) { $done = 1; } else { $ilp = $ilp . $_; } } # print "Read ILP:\n$ilp\n"; # kill 'KILL', $pid; # exit 0; # write ILP to a temporary file. $tmpfile = temporary_file(); open TMP, ">$tmpfile"; print TMP "$ilp"; close TMP; # invoke the solver on the temporary file # my $answer = `$solver $tmpfile`; my $answer = `matlab -nodisplay -nosplash -r "SolverILP('$tmpfile')" | tail -n +11`; print STDERR "Solver returned:\n$answer"; print WRITEME "$answer\n"; return; } sub temporary_file { my $name; my $fh; # try new temporary filenames until we get one that didn't already exist do { $name = tmpnam() } until $fh = IO::File->new($name, O_RDWR|O_CREAT|O_EXCL); return $name; } QCHECK/perl-cegar/cegar-solver-loop.pl~000755 000765 000024 00000005466 12332735011 021075 0ustar00fspedalistaff000000 000000 #!/usr/bin/env perl # This is the master command: wraps around the CEGAR model-checker and the # external ILP solver. See "cegar-solver-loop -u" for usage instructions. # use FindBin; use lib ( $FindBin::RealBin ); use IO::File; use POSIX qw(tmpnam); #use Expect; use IPC::Open2; use warnings; use Carp; use strict; use Getopt::Long; # give me a backtrace $SIG{ __DIE__ } = sub { Carp::confess( @_ ) }; our $model; our $solver; our $help = 0; # FIXME: later turn this to 0 our $verbose = 1; # process command-line options { my $result = GetOptions("model=s" => \$model, "solver=s" => \$solver, "verbose" => \$verbose, "help" => \$help, "usage" => \$help ); die "Error processing arguments" unless $result; } # sanity checking if ($help) { usage(); exit 0; } if (!$model) { print STDERR "Must specify model to process."; usage(); exit 1; } if (!$solver) { print STDERR "Must specify solver to handle ILPs."; usage(); #exit 1; } my $command; { my @args; if ($verbose) { push @args, "--verbose"; } # tell CEGAR loop to talk to an external program, not a user. push @args, "--programmatic"; push @args, $model; $command = join(" ",("aiger-cegar-test",@args)); } print "Starting:\n\t $command\n"; my $pid = open2(*README, *WRITEME, $command); while () { print STDERR "Read: $_"; if (m|----------------------------------------|) { print STDERR "Found start of ILP, invoking ilp_callback\n"; ilp_callback(); } } close(README); close(WRITEME); waitpid($pid, 0); exit 0; sub usage { print "$0 --model --solver \n"; print "\tPerform CEGAR model checking on , invoking the \n"; print "\tto solve any ILPs that arise in the process.\n"; } sub ilp_callback { # we have just read the top line of hyphens # read all of the rows my $ilp = ""; my $tmpfile; my $done = 0; while (!$done && ($_ = )) { if (m|----------------------------------------|) { $done = 1; } else { $ilp = $ilp . $_; } } # print "Read ILP:\n$ilp\n"; # kill 'KILL', $pid; # exit 0; # write ILP to a temporary file. $tmpfile = temporary_file(); open TMP, ">$tmpfile"; print TMP "$ilp"; close TMP; # invoke the solver on the temporary file # my $answer = `$solver $tmpfile`; my $answer = `matlab -nodisplay -nosplash -r "SolverILP('$tmpfile');exit" | tail -n +11`; print STDERR "Solver returned:\n$answer"; print WRITEME "$answer\n"; return; } sub temporary_file { my $name; my $fh; # try new temporary filenames until we get one that didn't already exist do { $name = tmpnam() } until $fh = IO::File->new($name, O_RDWR|O_CREAT|O_EXCL); return $name; } QCHECK/perl-cegar/eigk.S444.out000644 000765 000024 00000000511 12332735011 017066 0ustar00fspedalistaff000000 000000 ../tip-aig-20061215/eijk.S444.S.aig Done reading file and building model. Starting fixed point computation. Checking for goal Computing successors Checking for new state Checking for goal Computing successors Checking for new state Reached fixpoint after 2 steps Goal not reached No abstract path to goal state: circuit is safe. QCHECK/perl-cegar/eijk.S344.out000644 000765 000024 00000001177 12332735011 017101 0ustar00fspedalistaff000000 000000 ../tip-aig-20061215/eijk.S344.S.aig Done reading file and building model. Starting fixed point computation. Checking for goal Computing successors Checking for new state Checking for goal Computing successors Checking for new state Checking for goal Computing successors Checking for new state Checking for goal Computing successors Checking for new state Checking for goal Computing successors Checking for new state Checking for goal Computing successors Checking for new state Checking for goal Computing successors Checking for new state Reached fixpoint after 7 steps Goal not reached No abstract path to goal state: circuit is safe. QCHECK/perl-cegar/eijk.S349.out000644 000765 000024 00000000000 12332735011 017066 0ustar00fspedalistaff000000 000000 QCHECK/perl-cegar/eijk.S420.out000644 000765 000024 00000000000 12332735011 017054 0ustar00fspedalistaff000000 000000 QCHECK/perl-cegar/every_member_test.pl000644 000765 000024 00000002134 12332735011 021041 0ustar00fspedalistaff000000 000000 #! /usr/bin/env perl # Test reading and solving models formulated using AIGER use Aiger; use AigerModel; use Cudd; use ModelChecker; use Array::Compare; use strict; use warnings; use Carp; $SIG{ __DIE__ } = sub { Carp::confess( @_ ) }; # print "Model inputs: "; # print $model->inputs; # print "\n"; # print "Model outputs: "; # print $model->outputs; # print "\n"; # print "Model latches: "; # print $model->latches; # print "\n"; # print "Model and-gates: "; # print $model->andGates; # print "\n"; #exit 0; my $comp = Array::Compare->new; my @test_list1 = ( [0, 1, 2, 3], [ 2, 3], [ 1 , 2] ); my @test_list2 = ( [0, 1, 2, 3], [ 2, 3], [ 1 ] ); my @r1 = ModelChecker::every_member(@test_list1); my @r2 = ModelChecker::every_member(@test_list2); print "result 1: @r1\n"; die "r1 should check as true" unless @r1; die "r1 should be (2)" unless $comp->compare(\@r1, [2]); print "result 2: @r2\n"; die "r2 should check as false" if @r2; die "r2 should be empty" unless $comp->compare(\@r2, []); QCHECK/perl-cegar/exists-test.pl000644 000765 000024 00000001502 12332735011 017613 0ustar00fspedalistaff000000 000000 #! /usr/bin/env perl use Cudd; our $manager = new Cudd; our $v1 = $manager->BddVar; our $v2 = $manager->BddVar; our $v3 = $manager->BddVar; our $v4 = $manager->BddVar; our $v5 = $manager->BddVar; our $add = ($v1 ^ $v2) ^ ($v3 ^ $v4); $add->Print(1, 4); # $bdd->Compose(oldVar, newVar) our $newadd=$add->Compose($v4,$v5); $newadd->Print(1, 4); our $disj = $v1 + $v2 + $v3; $disj->Print(1,3); our $eq = Exists { $v1 } $disj; $eq->Print(1, 3); die "Existential quantification didn't work as expected" unless $eq == $manager->BddOne; print "AndExists test:\n"; our $econj1 = Exists { $v1 } $v1 * $v2 * $v3; $econj1->Print(1,4); our $tmp = $v1 * $v2; # $cube->AndExists(conjunct, other_conjunct) our $econj2 = $v1->AndExists($tmp,$v3); $econj2->Print(1,4); die "AndExists didn't work as expected" unless $econj1 == $econj2; exit 0; QCHECK/perl-cegar/hanoi-exercise.pl000755 000765 000024 00000022242 12332735011 020231 0ustar00fspedalistaff000000 000000 #!/usr/bin/env perl use Cudd; use warnings; use strict; our $verbose = 0; # throttle output... # Towers of Hanoi problem using BDDs our $SIZE = 10; # /* number of towers = 3 */ our $manager; #/* BDD Manager */ our @v1; # current state DdNode * v1[SIZE][3]; /* the current state */ our @v2; # DdNode * v2[SIZE][3]; /* the next state */ our @statevars; # build the skeleton of the 2D arrays for (my $i = 0; $i <= $SIZE; $i++) { push @v1, [ 0, 0, 0]; push @v2, [ 0, 0, 0]; } # /* v[i][j] = 1 means that disk i is in tower j */ sub make_a_move($$$); #DdNode * make_a_move(int i,int j,int k); sub compute_image($$$); #DdNode * compute_image(DdNode * R, DdNode * T, DdNode * cube); sub main { my $I; # /* the initial state BDD */ my $E; # /* the final state BDD */ my $T; # /* the transition relation */ my $R; my $image; my @images; # used to compute the counterexample... # int i,j,found,num_steps; #DdNode * tmp1, *tmp2; #DdNode * cube; #/* Initialize the BDD manager with default options */ $manager = new Cudd; #/* enable dynamic reordering */ $manager->EnableDyn(); # /* the current and next state variables are interleaved, usually a # good ordering to start with */ for(my $i=0;$i<$SIZE;$i++) { for(my $j=0;$j<3;$j++) { $v1[$i][$j] = $manager->BddVar; push @statevars, $v1[$i][$j]; $v2[$i][$j] = $manager->BddVar; } } #/* In the initial state, all the disks are in tower 0 */ $I = $manager->BddOne; for (my $i=0;$i<$SIZE;$i++) { $I = $I * $v1[$i][0]; } for (my $i=0;$i<$SIZE;$i++) { $I = $I * $v1[$i][1]->Not; } for (my $i=0;$i<$SIZE;$i++) { $I = $I * $v1[$i][2]->Not; } print "initialized Init state.\n" if $verbose; #/* In the final state, we want all the disks in tower 2 */ $E = $manager->BddOne; for (my $i=0;$i<$SIZE;$i++) { $E = $E * $v1[$i][2]; } for (my $i=0;$i<$SIZE;$i++) { $E = $E * $v1[$i][0]->Not; } for (my $i=0;$i<$SIZE;$i++) { $E = $E * $v1[$i][1]->Not; } print "initialized End state.\n" if $verbose; $T = $manager->BddOne; $T = $T->Not; # /* the transition relation is the disjunction of all possible moves */ for(my $i=0;$i<$SIZE;$i++) { for(my $j=0;$j<3;$j++) { my $tmp1 = make_a_move($i,$j,($j+1)%3); my $tmp2 = $T + $tmp1; $T = $tmp2; $tmp1 = make_a_move($i,$j,($j+2)%3); $tmp2 = $T + $tmp1; $T = $tmp2; } } print "initialized Transition matrix.\n" if $verbose; #/* Cube of the current state variables, needed by bddAndAbstract */ my $cube = $manager->BddOne; for(my $i=0;$i<$SIZE;$i++) { for(my $j=0;$j<3;$j++) { $cube = $cube * $v1[$i][$j]; } } print "initialized current state variable cube.\n" if $verbose; my $num_steps = 0; my $found = 0; # R contains the states reached so far, initialized to I $R = $I; print "Starting fixed point computation.\n" if $verbose; #/* Fixed point computation */ while(1) { #/* check if we reached the goal state */ my $tmp1 = $E->Not() + $R; print "Checking for goal\n" if $verbose; if ($tmp1 == $manager->BddOne) { print "Goal reached\n"; $found = 1; #/* goal reached */ last; } #/* compute the successors of the current state */ print "Computing successors\n" if $verbose; my $image = compute_image($R,$T,$cube); $num_steps ++; #/* check if we reached a new state */ #/* Note: Fixed point check, easy with BDDs as they are canonical */ print "Checking for new state\n" if $verbose; $tmp1 = $image->Not() + $R; if ($tmp1 == $manager->BddOne) { print "Reached fixpoint\n" if $verbose; last; #/* no new state reached */ } #/* add the new states to the reached set */ $tmp1 = $image + $R; push @images, $image; $R = $tmp1; } if ($found) { printf("Goal Reached in %d steps\n",$num_steps); # Cube of the successor state variables, needed by compute_counterexample my $cube = $manager->BddOne; for (my $i=0;$i<$SIZE;$i++) { for (my $j=0;$j<3;$j++) { $cube = $cube * $v2[$i][$j]; } } my @states = compute_counterexample(\@images, $E, $T, $cube); print "Counterexample:\n"; foreach my $state (@states) { foreach my $x (@$state) { print "$x"; } print "\n"; } } else { printf("Goal not reached\n"); } } # /* Returns a BDD representing move of disk i from tower j to tower k */ sub make_a_move ($$$)# (int i,int j,int k) { my $result; my $i = shift; my $j = shift; my $k = shift; # int l,m; # DdNode * tmp1; # DdNode * tmp2; $result = $v1[$i][$j]; # /* disk i is in tower j */ # /* this loop enforces that there is no smaller disk in tower j or tower k */ # /* no smaller disk in tower j implies that the disk at hand is at the top */ # /* no smaller disk in tower k implies that we can move the disk to tower k */ for(my $l=$i-1;$l>=0;$l--) { my $tmp1 = $result * $v1[$l][$j]->Not; $result = $tmp1; $tmp1 = $result * $v1[$l][$k]->Not; $result = $tmp1; } #/* move the current disk to tower k */ { my $tmp1 = $result * $v2[$i][$k]; $result = $tmp1; } { my $tmp1 = $result * $v2[$i][($k+1)%3]->Not; $result = $tmp1; } { my $tmp1 = $result * $v2[$i][($k+2)%3]->Not; $result = $tmp1; } #/* the other disks stay where they are */ for(my $l=0;$l<$SIZE;$l++) { if ($l!=$i) { for(my $m=0;$m<3;$m++) { my $tmp1 = $v1[$l][$m] ^ $v2[$l][$m]; $tmp1 = $tmp1->Not; # XNOR my $tmp2 = $result * $tmp1; $result = $tmp2; } } } return $result; } # /* Given a set of states R and a transition relation T, returns the BDD for the # states that can be reached in one step from R following T */ sub compute_image ($$$) #(DdNode * R, DdNode * T, DdNode * cube) { my $R = shift; my $T = shift; my $cube = shift; my $result; # /* the following Cudd function computes the conjunction of R and T; and quantifies out the variables # in cube ( the current state variables ) */ print "Calling AndExists\n" if $verbose; # $result = $cube->AndExists($R, $T); $result = Exists { $cube } $R * $T; print "Done with AndExists\n" if $verbose; print "Renaming next state variables\n" if $verbose; # /* rename the next state variables to the current state variables */ for(my $i=0;$i<$SIZE;$i++) { for(my $j=0;$j<3;$j++) { # /* compose replaces v2[i][j] with v1[i][j] */ my $tmp1 = $result->Compose($v2[$i][$j],$v1[$i][$j]); $result = $tmp1; } } print "Done renaming next state variables\n" if $verbose; return $result; } sub compute_preimage { # state, Transition relation, post variables my $state = shift; my $T = shift; my $postVarCube = shift; # take the state and rewrite the current state variables # to next state variables for(my $i=0;$i<$SIZE;$i++) { for(my $j=0;$j<3;$j++) { $state = $state->Compose($v1[$i][$j],$v2[$i][$j]); } } my $result = Exists { $postVarCube } $state * $T; return $result; } sub pick_state { my $bdd = shift; my $vars = shift; my @vars = @$vars; my @state; my $zero = $bdd->Zero; foreach my $var (@vars) { if ( ( $bdd * $var) != $zero) { $bdd = $bdd * $var; push @state, 1; } else { $bdd = $bdd * !$var; push @state, 0; } } return (\@state, $bdd); } sub compute_counterexample { my $imageptr = shift; my $endState = shift; my $T = shift; # transition relation my $postVarCube = shift; my @images = @$imageptr; my @preimages = (); my @states = (); my $image = pop(@images); $image = $endState * $image; my ($groundState, $state) = pick_state($image, \@statevars); push @states, $groundState; while (@images) { my $image = pop(@images); die "Image is Zero." if ($image == $image->Zero); my $preimage = compute_preimage($state, $T, $postVarCube); die "Preimage is inconsistent" if ($preimage == $preimage->Zero); $preimage = $preimage * $image; die "Preimage is inconsistent with image" if ($preimage == $preimage->Zero); my ($groundState, $stateBdd) = pick_state($preimage, \@statevars); push @states, $groundState; $state = $stateBdd; } ($groundState,$state) = pick_state($endState, \@statevars); push @states, $groundState; return reverse(@states); } &main(); =begin comment /* This example essentially illustrates reachability computation, which is one of the core operations inside a model checker. In model checking, the goal state represents the error state, and the model checker either: 1. Discovers that the error state is unreachable if the fixed point is achieved before hitting the error. 2. Discovers that the error is reachable. In that case it returns a counterexample, which is a sequence of steps from the initial state to the error state. The above implementation does not produce a counterexample. Exercise: Add counterexample generation to the above. How: You will need to store pointers to all the image BDDs. Starting from the error state, compute a "reverse image", intersect with the correspoding forward image, pick a state from the intersection and repeat till you hit the initial state. */ =end comment =cut QCHECK/perl-cegar/hanoi.pl000644 000765 000024 00000006536 12332735011 016431 0ustar00fspedalistaff000000 000000 #! /usr/bin/env perl # This is an example of using the new ModelChecker and Model perl libraries to # solve the Towers of Hanoi problem, which is solved also in the # hanoi-exercise.pl, which uses the Cudd library directly. use Model; use Cudd; use ModelChecker; use strict; use warnings; sub make_a_move($$$); my $model = new Model; my $manager = $model->manager(); my @statevars; my @nextstatevars; our @v1; # current state DdNode * v1[SIZE][3]; /* the current state */ our @v2; # DdNode * v2[SIZE][3]; /* the next state */ my $verbose=0; my $SIZE = 10; # build the skeleton of the 2D arrays for (my $i = 0; $i <= $SIZE; $i++) { push @v1, [ 0, 0, 0]; push @v2, [ 0, 0, 0]; } # /* the current and next state variables are interleaved, usually a # good ordering to start with */ for (my $i=0;$i<$SIZE;$i++) { for (my $j=0;$j<3;$j++) { $v1[$i][$j] = $manager->BddVar; push @statevars, $v1[$i][$j]; $v2[$i][$j] = $manager->BddVar; push @nextstatevars , $v2[$i][$j]; } } $model->set_state_vars(@statevars); $model->set_next_state_vars(@nextstatevars); my $I = $manager->BddOne; for (my $i=0;$i<$SIZE;$i++) { $I = $I * $v1[$i][0]; } for (my $i=0;$i<$SIZE;$i++) { $I = $I * $v1[$i][1]->Not; } for (my $i=0;$i<$SIZE;$i++) { $I = $I * $v1[$i][2]->Not; } $model->set_initial_state($I); #/* In the final state, we want all the disks in tower 2 */ my $E = $manager->BddOne; for (my $i=0;$i<$SIZE;$i++) { $E = $E * $v1[$i][2]; } for (my $i=0;$i<$SIZE;$i++) { $E = $E * $v1[$i][0]->Not; } for (my $i=0;$i<$SIZE;$i++) { $E = $E * $v1[$i][1]->Not; } print "initialized End state.\n" if $verbose; $model->set_target_state($E); my $T = $manager->BddOne; $T = $T->Not; # /* the transition relation is the disjunction of all possible moves */ for (my $i=0;$i<$SIZE;$i++) { for (my $j=0;$j<3;$j++) { my $tmp1 = make_a_move($i,$j,($j+1)%3); my $tmp2 = $T + $tmp1; $T = $tmp2; $tmp1 = make_a_move($i,$j,($j+2)%3); $tmp2 = $T + $tmp1; $T = $tmp2; } } print "initialized Transition matrix.\n" if $verbose; $model->set_transition_rel($T); ModelChecker::model_check($model); # /* Returns a BDD representing move of disk i from tower j to tower k */ sub make_a_move ($$$)# (int i,int j,int k) { my $result; my $i = shift; my $j = shift; my $k = shift; # int l,m; # DdNode * tmp1; # DdNode * tmp2; $result = $v1[$i][$j]; # /* disk i is in tower j */ # /* this loop enforces that there is no smaller disk in tower j or tower k */ # /* no smaller disk in tower j implies that the disk at hand is at the top */ # /* no smaller disk in tower k implies that we can move the disk to tower k */ for(my $l=$i-1;$l>=0;$l--) { my $tmp1 = $result * $v1[$l][$j]->Not; $result = $tmp1; $tmp1 = $result * $v1[$l][$k]->Not; $result = $tmp1; } #/* move the current disk to tower k */ { my $tmp1 = $result * $v2[$i][$k]; $result = $tmp1; } { my $tmp1 = $result * $v2[$i][($k+1)%3]->Not; $result = $tmp1; } { my $tmp1 = $result * $v2[$i][($k+2)%3]->Not; $result = $tmp1; } #/* the other disks stay where they are */ for(my $l=0;$l<$SIZE;$l++) { if ($l!=$i) { for(my $m=0;$m<3;$m++) { my $tmp1 = $v1[$l][$m] ^ $v2[$l][$m]; $tmp1 = $tmp1->Not; # XNOR my $tmp2 = $result * $tmp1; $result = $tmp2; } } } return $result; } QCHECK/perl-cegar/HiddenVarAigerModel.pm000644 000765 000024 00000022777 12332735011 021136 0ustar00fspedalistaff000000 000000 package HiddenVarAigerModel; use Cudd; use AigerModel; use parent Model; #use Scalar::Util; =head1 Name AbstractAigerModel - data structures for a model that is an abstraction of an underlying AigerModel =head1 Synopsis my $model = new AbstractAigerModel(model=>$model,show=>\@litsToShow) =head1 Description This model class attempts to make the hidden literals of the abstracted model simply invisible. In practice, this policy seems to conflict with the requirements of the CEGAR algorithm, so this class is deprecated. =head2 Functions =over =item new An HiddenVarAigerModel is made by passing a hash with initargs. Supported initargs include C, for the ground model, and C or C which contain lists of latch variables to either show or hide. In the former case, we treat the default as hiding all the latches, and in the latter it's the opposite. For example: my $abs = new HiddenVarAigerModel({model=>$model,show=>\@show}); or my $newModel = new HiddenVarAigerModel({model=>$model,hide=>\@hidden}); =cut # constructor method... sub new ($$) { die "The HiddenVarAigerModel class is deprecated. Please use AbstractAigerModel instead."; my $class = shift; my $initHashPtr = shift; my %initHash = %$initHashPtr; my $groundModel = $initHash{model} || die "Must specify a value for model in initializer for AbstractAigerModel."; my $showPtr = $initHash{show}; my $hidePtr = $initHash{hide}; die "Must specify list of literals to hide or to show." unless $showPtr || $hidePtr; my $self = {}; bless $self, $class; $self->{groundModel} = $groundModel; if ($showPtr) { $self->{shownLits} = $showPtr; my @hidden; foreach my $latch ($groundModel->latch_literals()) { my $found = grep {$_ == $latch} @$showPtr; push @hidden, $latch unless $found; } $self->{hiddenLits} = \@hidden; } elsif ($hidePtr) { $self->{hiddenLits} = $hidePtr; my @shown; foreach my $latch ($groundModel->latch_literals()) { my $found = grep {$_ == $latch} @$hidePtr; push @shown, $latch unless $found; } $self->{shownLits} = \@shown; } foreach my $l (@hidden) { die "Cannot hide a literal that is not a latch value, $l." unless $self->is_latch($l); } foreach my $l ($self->latch_literals()) { die "All latches must be shown or hidden" unless (grep {$_ == $l} @{$self->{hiddenLits}}) || (grep {$_ == $l} @{$self->{shownLits}}); } return $self; } # latches are pairs of literals sub add_latch ($$) { my $self = shift; die "Should never be adding a latch to an AbstractAigerModel, $self"; } sub add_output ($) { my $self = shift; die "Should never be adding an output to an AbstractAigerModel, $self"; } # although it doesn't line up with the latches, # we use literals for all three of the values here. sub add_andgate ($$$) { my $self = shift; die "Should never be adding an and gate to an AbstractAigerModel, $self"; } # $model->install_var($literal, $Bdd) sub install_var ($$) { my $self = shift; die "Should never be installing a variable on an AbstractAigerModel, $self"; } # start of delegated methods... =item $model->manager() Return the CUDD manager object corresponding to C<$model>. =cut sub manager { my $self = shift; my $groundModel = $self->{groundModel}; return $groundModel->manager(); } # sub all_vars { # my $self = shift; # my $groundModel = $self->{groundModel}; # return $groundModel->all_vars(); # } sub inputs { my $self = shift; my $groundModel = $self->{groundModel}; return $groundModel->inputs(); } sub outputs { my $self = shift; my $groundModel = $self->{groundModel}; return $groundModel->outputs(); } sub latches { my $self = shift; my $groundModel = $self->{groundModel}; return $groundModel->latches(); } sub andGates { my $self = shift; my $groundModel = $self->{groundModel}; return $groundModel->andGates(); } # FIXME: badly named -- the argument is a *literal*, not an index... sub is_var ($) { my $self = shift; my $literal = shift; my $groundModel = $self->{groundModel}; return $groundModel->is_var($literal); } sub is_negated ($) { my $self = shift; my $index = shift; my $groundModel = $self->{groundModel}; return $groundModel->is_negated($index); } # returns a one-based variable index (yuck!) sub var_index ($) { my $self = shift; my $index = shift; my $groundModel = $self->{groundModel}; return $groundModel->var_index($index); } sub decode_literal ($) { my $self = shift; my $lit = shift; my $groundModel = $self->{groundModel}; return $groundModel->decode_literal($lit); } sub target_state { my $self = shift; my $groundModel = $self->{groundModel}; my $target = $groundModel->target_state(); my $hvCube = $self->hiddenCube; $target = Exists {$hvCube} $target; return $target; } # all latches are initially zero... sub initial_state { my $self = shift; my $groundModel = $self->{groundModel}; my $init_state = $groundModel->initial_state(); my @latches = $groundModel->latches(); foreach my $l (@latches) { my ($old, $new) = @$l; if ($self->is_hidden($old)) { my $v = $self->decode_literal($old); $init_state = Exists {$v} $init_state; } } return $init_state; } sub is_latch ($) { my $self = shift; my $lit = shift; my $groundModel = $self->{groundModel}; die "No ground model for $self" unless $groundModel; return $groundModel->is_latch($lit); } =item latch_literals($m) Return a list of the latch literals that are I hidden in the model C<$m>. =cut sub latch_literals { my $self = shift; my $groundModel = $self->{groundModel}; die "No ground model for $self" unless $groundModel; my @literals = $groundModel->latch_literals(); my @unhidden; foreach my $l (@literals) { push @unhidden, $l unless $self->is_hidden($l); } return @unhidden; } # end of delegated methods sub state_vars { my $self = shift; my @vars; foreach my $latch ($self->latches()) { my ($old, $new) = @$latch; push @vars, $self->decode_literal($old) unless $self->is_hidden($old); } return @vars; } sub next_state_vars { my $self = shift; if (! $self->{_nextStateVarsSet}) { $self->initialize(); } my $vars = $self->{_nextStateVars}; return @$vars; } # Is the argument LITERAL hidden in the model? sub is_hidden ($) { my $self = shift; my $literal = shift; my $found = 0; die "Cannot hide a non-variable literal" unless $self->is_var($literal); foreach my $lit ( @{$self->{hiddenLits}} ) { if ($lit == $literal) { $found = 1; last; } } return $found; } sub initialize { my ( $self ) = @_; # cache the next state variables, # and they need to go in the transition relation... my @vars; my @literals; my $groundModel = $self->{groundModel} || die "No ground model for $self\n"; my $transitionRel = $groundModel->transition_rel(); my @latches = $groundModel->latches(); my @nsvars = $groundModel->next_state_vars(); die "Different number of latches ($#latches) from next state variables ($#nsvars)" unless $#latches == $#nsvars; for (my $i = 0; $i <= $#latches; $i ++) { my $latch = $latches[$i]; my $nsvar = $nsvars[$i]; my ($old, $new) = @$latch; if ($self->is_hidden($old)) { my $oldvar = $self->decode_literal($old); $transitionRel = Exists {$oldvar} $transitionRel; $transitionRel = Exists {$nsvar} $transitionRel; } else { # this latch is not hidden push @vars, $nsvar; } } $self->{_nextStateVars} = \@vars; $self->{_transitionRel} = $transitionRel; $self->{_nextStateVarsSet} = 1; } sub transition_rel { my $self = shift; if (! $self->{_nextStateVarsSet}) { # need to cache the transition relation $self->initialize(); } return $self->{_transitionRel}; } sub inputCube { my $self = shift; my @inputVars = $self->inputVars; my $manager = $self->manager(); my $cube = $manager->BddOne; foreach my $var (@inputVars) { $cube = $cube * $var; } return $cube; } # In the Abstract Aiger model, some latches are treated as if they are inputs, # but in the HiddenVarAigerModel they are simply removed and the inputVars are # as per the base model. sub inputVars { my $self = shift; my $groundModel = $self->{groundModel}; return $groundModel->inputVars(); } sub latchVars { my $self = shift; my @latches = $self->latches(); my @vars; foreach my $latch (@latches) { my ($old, $new) = @$latch; if (! $self->is_hidden($old)) { push @vars, $self->decode_literal($old); } } return @vars; } sub now_vars { my $self = shift; my $groundModel = $self->{groundModel}; my @now_vars = $groundModel->now_vars(); my @latches = $self->latches(); foreach my $latch (@latches) { my ($old, $new) = @$latch; if ($self->is_hidden($old)) { push @now_vars, $self->decode_literal($old); } } return @now_vars; } =item $model->hidden_vars() Returns a list of the variables (BDD nodes) corresponding to literals hidden in C<$model>. Primarily of use as a debugging tool. =cut sub hidden_vars { my $self = shift; my @hidden = @{$self->{hiddenLits}}; my @vars; foreach my $h (@hidden) { push @vars, $self->decode_literal($h); } return @vars; } =item $model->hiddenCube() Returns a cube (BDD) of the literals hidden in C<$model>. Primarily of use as a debugging tool. =cut sub hiddenCube { my $self = shift; my @vars = $self->hidden_vars(); die "No hidden vars for model $self." unless @vars; my $bdd = $vars[0]->One; foreach my $var (@vars) { $bdd = $bdd * $var; } return $bdd; } 1; QCHECK/perl-cegar/ilp-clean.lisp000644 000765 000024 00000001271 12332735011 017522 0ustar00fspedalistaff000000 000000 (in-package :cl-user) (require 'iterate) (defun ilp-read (file) (with-open-file (str file) (iter (for x = (read-line str nil nil)) (while x) (collecting (iter (with pos = 0) (with n) (multiple-value-setq (n pos) (parse-integer x :start pos :junk-allowed t)) (while n) (collecting n)))))) (defun ilp-filter (lst) (let ((l1 (remove-duplicates lst :test 'equal))) (iter (for (x . rest) on l1) (unless (some #'(lambda (y) (subsetp y x)) rest) (collecting x))))) (defun ilp-print (lst) (iter (for sublist in lst) (format t "~{~2d~^ ~}~%" sublist))) QCHECK/perl-cegar/ken.flash.02.out000644 000765 000024 00000000000 12332735011 017574 0ustar00fspedalistaff000000 000000 QCHECK/perl-cegar/make-docs.pl000755 000765 000024 00000001367 12332735011 017176 0ustar00fspedalistaff000000 000000 #! /usr/bin/env perl # This is a crude and not-portable script for building HTML documents for the # Qcheck CEGAR program. But it isn't too hard to configure. Just set the # following three variables, and it should Do The Right Thing. [2014/01/13:rpg] my $perlCegarDirectory = "."; my $perlDDInstallDirectory = "/Users/rpg/src/PerlDD-0.09"; my $output_dir = "./htmldocs/"; # End of configuration variables my $perlDDDirectory = $perlDDInstallDirectory . "/blib/lib/"; use Pod::Simple::HTMLBatch; my $batchconv = Pod::Simple::HTMLBatch->new; my @search_dirs = ( $perlCegarDirectory, $perlDDDirectory); #$batchconv->some_option( some_value ); #$batchconv->some_other_option( some_other_value ); $batchconv->batch_convert( \@search_dirs, $output_dir ); QCHECK/perl-cegar/Model.pm000644 000765 000024 00000010313 12332735011 016360 0ustar00fspedalistaff000000 000000 package Model; use Cudd; =head1 Name Model - data structures for a model suitable for use with the ModelChecker module. =head1 Synopsis my $model = new Model(); $model->set_state_vars(@vars); $model->set_next_state_vars(@nsvars); $model->set_initial_state($state); $model->set_target_state($tstate); ModelChecker::model_check($model) =head1 Description Somewhat generic model-checking, based on the L Perl DD library, executed by code in the L module. =head2 Functions =over =cut sub new { my $class = shift; my $self = {}; my $manager = new Cudd; $self->{_manager} = $manager; bless $self, $class; return $self; } sub manager { my ( $self ) = @_; return $self->{_manager}; } =item state_vars C<< $model->state_vars() >> Returns a list of variables (singleton BDDs) for the state variables of C<$model>. In systems with a distinction between persistent state variables and inputs, this method will I return the inputs; only the state variables. If you want the full set of variables that characterize the state of the system, I inputs, use L instead. =cut sub state_vars { my ( $self ) = @_; my $varptr = $self->{_state_vars}; return @$varptr; } # by default, now_vars == the state_vars, but in some models there may be # additional variables that are not part of the state (i.e., that do not # persist, so do not have corresponding next_state_vars). =item now_vars C<< $model->now_vars() >> Return a list of the variables that need to be existentially quantified away in order to be left with the next state variables when doing state progression. By default, this list will be the same as C<$self->state_vars()), but some subclasses may override that. This would be necessary if there are some variables in the current state that do not appear in the C. In turn that can happen if there are some variables that do not persist, as in AIGER models. =cut sub now_vars { my ( $self ) = @_; return $self->state_vars(); } sub next_state_vars { my ( $self ) = @_; my $varptr = $self->{_next_state_vars}; return @$varptr; } sub set_state_vars { my($self, @state_vars) = @_; $self->{_state_vars} = \@state_vars; return $self->state_vars; } sub set_next_state_vars { my($self, @next_state_vars) = @_; $self->{_next_state_vars} = \@next_state_vars; return $self->next_state_vars; } sub initial_state { my ( $self ) = @_; return $self->{_initial_state}; } sub set_initial_state { my($self, $state) = @_; $self->{_initial_state} = $state; return $self->{_initial_state}; } sub target_state { my ( $self ) = @_; return $self->{_target_state}; } sub set_target_state { my($self, $state) = @_; $self->{_target_state} = $state; return $self->{_target_state}; } sub transition_rel { my ( $self ) = @_; return $self->{_transition_rel}; } sub set_transition_rel { my($self, $state) = @_; $self->{_transition_rel} = $state; return $self->{_transition_rel}; } sub BddVar { my ( $self ) = @_; return $self->manager->BddVar; } sub is_bdd { my ( $self, $putativeBdd ) = @_; return $putativeBdd->isa("Cudd::BDD"); } sub this_state_cube { my $self = shift; if ( ! defined($self->{_stateCube} ) ) { my $manager = $self->manager(); my $cube = $manager->BddOne; foreach my $v ($self->now_vars()) { $cube = $cube * $v; } $self->{_stateCube} = $cube; } return $self->{_stateCube}; } sub next_state_cube () { my $self = shift; if ( ! defined($self->{_nsCube}) ) { my $manager = $self->manager(); my $cube = $manager->BddOne; foreach my $v ($self->next_state_vars()) { $cube = $cube * $v; } $self->{_nsCube} = $cube; } return $self->{_nsCube}; } sub latch_cube { my $self = shift; my $manager = $self->manager(); my $cube = $manager->BddOne; foreach my $v ($self->state_vars()) { $cube = $cube * $v; } return $cube; } =item make_cube $m->make_cube(@varlist) Returns a BDD that is the cube made from the varlist. =cut sub make_cube { my $self = shift; my @vars = @_; my $manager = $self->manager(); my $cube = $manager->BddOne; foreach my $v (@vars) { $cube = $cube * $v; } return $cube; } =back =cut 1; QCHECK/perl-cegar/ModelChecker.pm000755 000765 000024 00000105476 12332735011 017667 0ustar00fspedalistaff000000 000000 #!/usr/bin/env perl =head1 Name ModelChecker -- perl utilities for OBDD-based model-checking =head1 Synopsis my $model = Aiger::read_aig_file($ARGV[0]); ModelChecker::model_check($model); or ModelChecker::cegar_model_check($model); =head1 Description Somewhat generic model-checking, based on the L Perl DD library. Only handles reachability model-checking and will not work unless using an AIGER-based model (see L). Offers two options: a simple reachability model checking, C, and a (only semi-implemented) version of the CEGAR counter-example guided abstraction refinement =head2 Functions =over =cut package ModelChecker; require Exporter; @ISA = qw(Exporter); @EXPORT_OK = qw(model_check cegar_model_check verbose interactive); use Cudd; use warnings; use strict; use Model; use AigerModel; use AbstractAigerModel; use HiddenVarAigerModel; use Array::Utils qw{intersect}; our $verbose = 0; # throttle output... our $cautious = 1; our $interactive = 1; our $manager; #/* BDD Manager */ our $debugMode = defined &DB::DB; sub compute_image($$;$); # state, model, limiting state (optional) sub compute_preimage ($$); # state, model sub pick_state ($$); # BDD, pointer to variable list sub cegar_model_check ($); # pointer to AigerModel sub model_check ($); # pointer to Model (could be AigerModel) sub check_abs_path ($@); # pointer to ground model, list of images sub refine_abstraction($$$$); # abstract model, deadEnd BDD, image list (ptr) and index of unreachable image sub nonempty($); # is BDD argument nonempty (i.e., != Zero)? sub progress_statevars ($$); sub regress_statevars ($$); sub aiger_counterexample ($$$); # ptr to image list, end state BDD, model sub print_counterexample(@); #helper function sub compute_counterexample ($$$); # ptr to image list, end state BDD, model sub state_gen ($$@); sub verbose ($) { $verbose = shift; } sub interactive ($) { $interactive = shift; if (!$interactive) { # make sure you flush output... $| = 1; } } sub model_check ($) { my $model = shift; die "Model not of expected type." unless $model->isa("Model"); my $I = $model->initial_state; # the initial state BDD my $E = $model->target_state; # /* the final state BDD */ # print STDERR "Target state is $E\n"; print STDERR "Making transition relation\n" if $verbose; my $T = $model->transition_rel; # /* the transition relation */ print STDERR "Done making transition relation\n" if $verbose; my $R; # reachable states BDD my $Core; # "core" BDD of latch values used to # generate successor states. my $image; my @images; # used to compute the counterexample... print STDERR "Preparing for model-checking.\n" if $verbose; $manager = $model->manager(); #/* enable dynamic reordering */ $manager->EnableDyn(); # This fails if $E->Not() is a tautology. [2013/10/15:rpg] if ($E == $manager->BddOne) { print "target state is vacuously true.\n"; exit 0; } elsif ($E->Not() == $manager->BddOne) { print "target state is vacuously false.\n"; exit 0; } if (( $I->Or($E->Not()) ) == $manager->BddOne) { print STDERR "Negated target state is:\n"; $E->Not()->Print(1, 3); print STDERR "Initial state is:\n"; $I->Print(1, 3); if ($I->Equal($E->Not()) ) { # this should be true... print "Initial state is the negation of the target state\n"; } elsif ($I->Equal($E) ) { print "Initial state is the target state\n"; } my @vars = $model->now_vars(); my ($stateref, $bdd) = pick_state($I, \@vars); my @state = @{$stateref}; print "Pick state returns: @state\n"; return 1; } # print STDERR "Building cube of current state variables\n" if $verbose; # #/* Cube of the current state variables, needed by bddAndAbstract */ # my $cube = $model->this_state_cube(); # print STDERR "initialized current state variable cube.\n" if $verbose; # print STDERR "Building cube of next state variables\n" if $verbose; # my $nsCube = $model->next_state_cube(); # print STDERR "initialized next state variable cube.\n" if $verbose; my $num_steps = 0; my $found = 0; # R contains the states reached so far, initialized to I $R = $I; push @images, $R; # get the initial state onto the images list print "Starting fixed point computation.\n" if $verbose; # $DB::single = 1; #/* Fixed point computation */ while (1) { my $tmp1; my $tmp2; my $tmp3; my $image; #/* check if we reached the goal state */ print "Checking for goal\n" if $verbose; if ( ($E * $R) != $E->Zero ) #(($E->Not + $R) == $E->One) { print "Goal reached\n"; $found = 1; #/* goal reached */ last; } #/* compute the successors of the current state */ print "Computing successors\n" if $verbose; $image = compute_image($R,$model); $num_steps ++; #/* check if we reached a new state */ #/* Note: Fixed point check, easy with BDDs as they are canonical */ print "Checking for new state\n" if $verbose; $tmp2 = $image->Not() + $R; if ($tmp2 == $manager->BddOne) { print "Reached fixpoint after $num_steps steps\n" if $verbose; last; #/* no new state reached */ } #/* add the new states to the reached set */ $tmp3 = $image + $R; push @images, $image; $R = $tmp3; } my ($statesptr,$bddstateptr); # for catching the counterexample return values. if ($found) { printf("Goal Reached in %d steps\n",$num_steps); { # make sure the final state of the images hits the goal my $i = $#images; $images[$i] = $images[$i] * $E; } if ($num_steps > 0) { my @imagecopy = @images; ($statesptr,$bddstateptr) = compute_counterexample(\@imagecopy, $E, $model); print "Counterexample:\n"; foreach my $state (@$statesptr) { print $state; } } } else { printf("Goal not reached\n"); } return $found, \@images; } =item invert_image_vector($model, $imageListPtr) Take the list of images, made by progression from the initial state (which should be =C<${$imageListPtr}[0]>), generate and return a new counterexample trace by regressing the end state (which must satisfy =C<$model->target_state()>) back to the initial state. This fixes a problem where the original trace is not limited to states that can eventually lead to the target state. =cut sub invert_image_vector ($$) { my $model = shift; my $imagelistPtr = shift; my @imagelist = @{$imagelistPtr}; my @newimages; my @latches = $model->latchVars(); # for debugging... my $latchCube = $model->make_cube(@latches); my $inputCube = $model->inputCube(); my @groundStates; my $image = pop(@imagelist); my ($groundState, $state) = pick_state($image, \@latches); push @newimages, $state; push @groundStates, $groundState; while (@imagelist) { my $image = pop(@imagelist); die "Image is Zero." if ($image == $image->Zero); # note that the image structure may have some extra variables in the case # where it's the initial state... if ($cautious) { die "Extraneous variables in state structure" unless ( ( $state->Support->LiteralSetIntersection($latchCube) ) == $state->Support ); } my $preimage = compute_preimage($state, $model); die "Preimage is inconsistent" if ($preimage == $preimage->Zero); $preimage = $preimage * $image; die "Preimage is inconsistent with image" if ($preimage == $preimage->Zero); if (! @imagelist) { # we are at the initial state $preimage = $preimage * $model->initial_state(); die "First image is inconsistent with the ground model initial state" if ($preimage * $model->{groundModel}->initial_state == $preimage->Zero); } my ($groundState, $stateBdd) = pick_state($preimage, \@latches); $stateBdd = Exists {$inputCube} $stateBdd; push @newimages, $stateBdd; push @groundStates, $groundState; $state = $stateBdd; } if ($verbose > 0) { print "Abstract counterexample:\n"; foreach my $groundState (reverse(@groundStates)) { my $latchString = join "", @{$groundState}; printf "\t%s\n", $latchString; } } return reverse(@newimages); } sub cegar_model_check ($) { my $model = shift; # pointer to AigerModel die "cegar_model_check only implemented for AigerModels" unless $model->isa("AigerModel"); my $abs = initial_abstraction($model); my $found; my @images; my $imgptr; while (1) { { my @hidden = @{$abs->{hiddenLits}}; print STDERR "Checking abstract model, hidden literals are: @hidden\n"; if ( ! @hidden ) { print STDERR "Degenerate case of CEGAR model checking: no hidden literals.\n"; return model_check($model); } } ($found, $imgptr) = model_check($abs); if (! $found) { print "No abstract path to goal state: circuit is safe.\n"; last; } else { @images = invert_image_vector($abs,$imgptr); # the images above are a raw sequence of images from the forward # reachability search. We will reformulate them to get an abstract # counterexample (where only the visible variables are grounded). That # will drive our refinement process. my ($invalid, $deadEnd) = check_abs_path($model,@images); if ( !$invalid ) { print "Abstract counterexample is valid.\n"; last; } else { print "Abstract counterexample is invalid at step $invalid.\n"; $abs = refine_abstraction($abs, $deadEnd, \@images, $invalid); } } } return $found; } =item abstract_images($abstractModel, @imageList) Return a new list of images (BDDs), corresponding to c<@imageList>, but abstracted according to the abstract model. =cut # FIXME: rewrite this to use abstract_state. Also modify AbstractAigerModel so # that the hiddenCube is memoized. sub abstract_images ($@) { my ($absModel, @images) = @_; my @retval; my $hiddenCube = $absModel->hiddenCube(); foreach my $img (@images) { my $new = Exists { $hiddenCube } $img; push @retval, $new; } return @retval; } =item abstract_images($abstractModel, $BDD) Return a new state (BDD), corresponding to c<$BDD>, but abstracted according to the abstract model, c<$abstractModel>. =cut sub abstract_state ($$) { my ($absModel, $bdd) = @_; my $hiddenCube = $absModel->hiddenCube(); return Exists {$hiddenCube} $bdd; } sub initial_abstraction ($) { my $model = shift; my @show = $model->init_latches_to_show(); my $abs = new AbstractAigerModel({model=>$model,show=>\@show}); # my $abs = new HiddenVarAigerModel({model=>$model,show=>\@show}); return $abs; } =item check_abs_path($M, @images) Takes a path of I images, and the I model, C<$M> underlying them and checks to see if the path of images is a valid counterexample for the ground model. If it is I valid, returns two values: =over =item 1. The index of the bad state (this should always be greater than or equal to one). =item 2. The BDD for the last valid ground state (this will be a concrete state corresponding to the abstract state immediately prior to the index returned. =back If the counterexample is valid, this subroutine will return zero. =cut sub check_abs_path ($@) { my $groundModel = shift; my @images = @_; my $S; # CUDD BDD my $Sprev; # $S = h-1($s1) * $groundModel->initial_state(); $S = $groundModel->initial_state(); $S = $S * $images[0]; die "Invalid initial state." unless nonempty($S); # j starts at 1 (incremented at top of loop) because the zeroth image has # already been used my $j = 0; while (nonempty($S) && $j < $#images) { $j++; $Sprev = $S; $S = compute_image($S, $groundModel); $S = $S * $images[$j]; } if (nonempty($S) ) { return 0; } else { return $j, $Sprev; } } =item refine_abstraction($absModel, $deadEnd, $imageptr, $i) The arguments should be: =over =item the abstracted model object, =item the dead end state computed by "playing back" the abstract counterexample in the ground model, =item a pointer to the list of images in the abstract reachability graph to the target state and =item the index in the images of the unreachable state (one past the dead end state). =back as a side-effect, prints an ILP. Returns a new refined (but still, in general, abstract) model. =cut # <> sub refine_abstraction($$$$) { # abstract model, deadEnd BDD, images list and index of unreachable state my $absModel = shift; my $deadEnd = shift; # *concrete* dead end state in faulty counterexample my $imageptr = shift; my $unreachableIndex = shift; my @images = @$imageptr; # a list of abstract states, the (faulty) abstract counterexample my $newModel; my $prefilter; my $groundModel = $absModel->{groundModel}; # $bad == ground states that are in the pre-image of the unreachable state my $absUnreachable = $images[$unreachableIndex]; if ($absModel->isa("AbstractAigerModel")) { # $absUnreachable = Exists {$absModel->hiddenCube} $absUnreachable; $absUnreachable = Exists {$groundModel->inputCube} $absUnreachable; } my $bad = compute_preimage($absUnreachable, $groundModel); die "No preimage of unreachable state." if $bad == $bad->Zero; $bad = Exists {$groundModel->inputCube} $bad; $prefilter = $images[$unreachableIndex-1]; if ($absModel->isa("AbstractAigerModel")) { $prefilter = Exists {$absModel->hiddenCube} $prefilter; $prefilter = Exists {$absModel->inputCube} $prefilter; } $bad = $bad * $prefilter; if ($bad == $bad->Zero) { $DB::single=1; } die "No bad states." if $bad == $bad->Zero; die "Dead End states and bad states are not mutually exclusive" unless ($bad * $deadEnd) == $bad->Zero; # for now, just dump an ILP: my @hidden ; my @hlits; # need to remove irrelevant literals... # FIXME: this code is ugly because I butchered it in -- should be pulled out { my $sos = $deadEnd->Support()->LiteralSetIntersection($bad->Support()); my @vars = $absModel->hidden_vars(); my @lits = @{$absModel->{hiddenLits}}; for (my $i = 0; $i <= $#vars; $i++) { # var is in the set of support if ( $vars[$i]->LiteralSetIntersection($sos) == $vars[$i] ) { push @hidden, $vars[$i]; push @hlits, $lits[$i]; } } } my $deGen = state_gen($deadEnd, $groundModel, @hidden); my $deState; my @rows; print "ILP is:\n"; my $showLiteral; while (defined($deState=$deGen->())) { print STDERR "Comparing dead end state @{$deState}\n" if $verbose > 2; my $badGen = state_gen($bad, $groundModel, @hidden); my $badState; while (defined($badState=$badGen->())) { print STDERR "\tcomparing to bad state @{$badState}\n" if $verbose > 2; my @row; for (my $i = 0; $i <= $#hlits; $i++) { if (${$deState}[$i] != ${$badState}[$i]) { # print "$hlits[$i] "; push @row, $hlits[$i]; } } if (!@row) { warn "No difference between states @{$deState} and @{$badState}" unless @row; next; } print STDERR "\tNew row @row\n" if $verbose > 2; { my $found = 0; foreach my $other (@rows) { if ( is_subset($other,\@row) ){ $found = 1; last; } } if (! $found) { push @rows, \@row; print "@row\n"; } else { print STDERR "Row @row subsumed by previous entry.\n" if $verbose > 2 } } } } @rows = remove_redundant(@rows); my @common = every_member(@rows); if (@common) { $showLiteral = $common[0]; die "Error picking an intersection literal" unless $showLiteral; print STDERR "Splitting on literal $showLiteral\n" if $verbose; $newModel = simple_refinement($absModel,$showLiteral); } else { print STDERR "No common element in ILP. Enter literals to split on.\n"; print STDERR "Calling print_ilp\n"; print_ilp(@rows); print STDERR "Returned from print_ilp\n"; my $done = 0; my @fields; while (! $done) { my $split; chomp ($split = ); @fields = split /[\s,]+/, $split; print STDERR "Will split on:\n"; foreach my $field (@fields) { print STDERR "$field "; } if ($interactive) { print "\nOK? "; my $ans; chomp ($ans = ); $done = ($ans eq "y") || ($ans eq "Y"); } else { # if working with a program, instead of a user, we are just done $done = 1; } } print STDERR "Splitting on @fields\n" if $verbose; $newModel = $absModel; foreach my $field (@fields) { $newModel = simple_refinement($newModel, $field); } } return $newModel; } =item every_member Take a list of lists (list of list pointers) as argument. Return a list of elements that appear in every list. =cut sub every_member (@) { my @list = @_; my @first_list = @{$list[0]}; my @rest = @list[1..$#list]; my @retval = @first_list; map { @retval = intersect(@retval, @{$_}); } @rest; return @retval; } =item simple_refinement($oldAbsModel,$literalToShow) Make and return a simple refined model derived from C<$oldAbsModel> by un-hiding C<$literalToShow>. =cut sub simple_refinement ($$) { my ($oldAbsModel,$literalToShow) = @_; my @shown = @{$oldAbsModel->{shownLits}}; push @shown,$literalToShow; @shown = sort {$a <=> $b} @shown; my $newModel = new AbstractAigerModel({model=>$oldAbsModel->{groundModel}, show=>\@shown}); # my $newModel = new HiddenVarAigerModel({model=>$oldAbsModel->{groundModel}, # show=>\@shown}); die "Showing not working" if $newModel->is_hidden($literalToShow); return $newModel; } =item all_states($BDD, $Model, @variables) Use the state generator (created by L) to compute all the assignments to C<@variables> consistent with c<$BDD>. =cut sub all_states ($$@) { my ($bdd,$model, @vars) = @_; my $gen = state_gen($bdd,$model,@vars); my @res; my $s; while (defined($s = $gen->())) { push @res,$s; } return @res; } =item state_gen($BDD, $Model, @variables) Return a generator for states from a BDD, given variables. =cut sub state_gen ($$@) { my ($bdd, $model, @vars) = @_; # my @vars; # foreach my $lit (@lits) { # push @vars, $model->decode_literal($lit); # } my @arr = (0) x ($#vars + 1); my $done = 0; return sub { return undef if ($done); my $found = 0; my $asgn; my $retval; while (1) { ($found, $asgn) = next_state($model, $bdd, \@vars, \@arr); @$retval = @$asgn; # print "Found value is $found for @$asgn\n"; $done = incr_state(\@arr); # prepare for next # print "Done value is $done\n"; last if ($found); last if ($done); } if ($found) { # print "Found so returning @$retval\n"; return $retval; } elsif ($done) { return undef; } } } =item next_state($model, $bdd, $varptr, $valptr) Helper function for the state_gen iterator. Should not be called directly. =C<$varptr> is a pointer to a list of variables, and =C<$valptr> a pointer to a list of variable values (1 or zero). =cut sub next_state ($$$$) { my ($model, $bdd, $varptr, $valptr) = @_; my $found = 1; my @vars = @$varptr; my @vals = @$valptr; for (my $i = 0; $i <= $#vars; $i++) { # print "checking var value $i\n"; if ($vals[$i] == 0) { $bdd = $bdd * !$vars[$i]; } else { $bdd = $bdd * $vars[$i]; } if ($bdd == $bdd->Zero) { $found = 0; last; } } return $found, $valptr; } # side effects to increment the binary vector in its # (pointer) argument. Returns a boolean indicating whether # the array has overflowed. sub incr_state($) { my $arr = shift; my @array = @$arr; my $carry = 1; for (my $i = 0; $i <= $#array; $i++) { my $tmp = ${$arr}[$i] ^ $carry; $carry = ${$arr}[$i] & $carry; ${$arr}[$i] = $tmp; } return $carry; } # /* */ =item compute_image($R, $M) Given a set of states, C<$R> and a Model, C<$M>, returns the BDD for the states that can be reached in one step from C<$R> following the transition relation of C<$M>. =cut sub compute_image ($$;$) # $R - reachable states, $M - model, optional limiting state { my ($R, $M, $limit) = @_; # FIXME: in AIGER mode, there may be this state variables that need to be # removed when progressing the state that are NOT latch variables (so don't # get rewritten). Fix by using class-specific progression methods? my $cube = $M->this_state_cube(); my $T = $M->transition_rel(); my $result; # /* the following Cudd function computes the conjunction of R and T; and quantifies out the variables # in cube ( the current state variables ) */ print "Calling AndExists\n" if $verbose >= 2; $result = Exists { $cube } $R * $T; # $result = $cube->AndExists($R, $T); <- couldn't get this to work print "Done with AndExists\n" if $verbose >= 2; if (defined $limit) { # FIXME: think this may be applying limiting to the wrong state -- it's a mess. warn_or_die("Limiting logic may not yet work."); $result = $result * $limit; } # FIXME: big heap of debugging code. Need to remove it eventually. # { # my $supp = $nextCore->Support(); # if ( ! ($nsCube == $supp ) ) { # my $inputCube = $M->inputCube(); # my $intersection = $inputCube->LiteralSetIntersection($supp); # if (! $intersection->Equal($supp->One)) { # # Cudd::BDD::Dot([$inputCube]); # # Cudd::BDD::Dot([$supp]); # # Cudd::BDD::Dot([$intersection]); # die "There's a non-empty intersection between the support and the set of inputs."; # } # print "Next State Cube:\n"; # Cudd::BDD::Dot([$nsCube]); # print "Next core support cube:\n"; # Cudd::BDD::Dot([$supp]); # die "Support of the AndExists is not the same as the next state variables.\n"; # } # } die "Result not a BDD" unless $M->is_bdd($result); print "Renaming next state variables\n" if $verbose >= 2; # /* rename the next state variables to the current state variables */ $result = progress_statevars($M, $result); print "Done renaming next state variables\n" if $verbose >=2; return $result; } =item progress_statevars ($Model, $BDD) Replace the next state variables in C<$BDD> with current state variables, according to C<$Model>. Returns a new BDD. In order for this to be correctly used, the next statevars should not already be present. =cut # <> sub progress_statevars ($$) { my ($M, $Bdd) = @_; my @statevars = $M->state_vars(); my @next_statevars = $M->next_state_vars(); if ($cautious) { if ($Bdd->Support()->LiteralSetIntersection($M->make_cube(@statevars)) != $Bdd->One) { die "Calling progress_statevars on an unprepared state -- current statevars should be quantified away."; } } die "Number of new and old state variables disagree in cardinality." unless $#statevars == $#next_statevars; for (my $i = 0; $i <= $#statevars; $i++) { # print "$i\n"; die "Type error" unless $M->is_bdd($next_statevars[$i]) && $M->is_bdd($statevars[$i]); # $next_statevars[$i]->Print(1,2); # $statevars[$i]->Print(1,2); my $tmp1 = $Bdd->Compose($next_statevars[$i], $statevars[$i]); $Bdd = $tmp1; } return $Bdd; } =item regress_statevars ($Model, $BDD) The opposite of =L, here we replace the current state variables in C<$BDD> with next state variables, according to C<$Model>. Returns a new BDD. =cut # <> sub regress_statevars ($$) { my ($M, $Bdd) = @_; my @statevars = $M->state_vars(); my @next_statevars = $M->next_state_vars(); if ($cautious) { if ($Bdd->Support()->LiteralSetIntersection($M->make_cube(@next_statevars)) != $Bdd->One) { die "Calling regress_statevars on an unprepared state -- next state variables should be quantified away."; } } die "Number of new and old state variables disagree in cardinality." unless $#statevars == $#next_statevars; for (my $i = 0; $i <= $#statevars; $i++) { # print "$i\n"; die "Type error" unless $M->is_bdd($next_statevars[$i]) && $M->is_bdd($statevars[$i]); # $next_statevars[$i]->Print(1,2); # $statevars[$i]->Print(1,2); my $tmp1 = $Bdd->Compose($statevars[$i],$next_statevars[$i]); $Bdd = $tmp1; } return $Bdd; } =item compute_preimage($Bdd, $Model) Return a new BDD that represents the preimage of =C<$Bdd> according to =C<$Model>. The resulting BDD will be a boolean function of current state variables (e.g., latches), and inputs. This is appropriate for computing a counterexample, but if it were to be used in computing backwards reachability, probably the inputs should be quantified away before using the result. =cut sub compute_preimage ($$) { # state, Model my $state = shift; my $M = shift; my $T = $M->transition_rel(); my $postVarCube = $M->next_state_cube(); if ($cautious) { die "Attempting to compute the preimage of a state including excess variables." unless ( $state->Support->LiteralSetIntersection($M->make_cube($M->state_vars())) == $state->Support() ); # we should have only state variables here -- not even extended state # variables (e.g., with inputs) } # successor state with the current state variables turned into next # state variables where appropriate my $succ_state = regress_statevars($M, $state); # the following looks like voodoo programming; removing this call as unnecessary. [2014/01/09:rpg] # # now we remove all the remaining state variables # $succ_state = Exists { $M->this_state_cube } $succ_state; # now we should have a bunch of post-state variables. # Regress them over the transition relation and return the # resulting state. my $result = Exists { $postVarCube } $succ_state * $T; return $result; } =item pick_state($BDD, $varlistPtr) Return two values: the first is a pointer to a list of boolean values indicating the assignment of values to the variables in the variable list. The second is a BDD representing this assignment in the context of $BDD. =cut sub pick_state ($$) { my $bdd = shift; my $vars = shift; my @vars = @$vars; my @state = (); my $zero = $bdd->Zero; foreach my $var (@vars) { if ( ( $bdd * $var) != $zero) { $bdd = $bdd * $var; push @state, 1; } else { $bdd = $bdd * !$var; push @state, 0; } } return (\@state, $bdd); } sub compute_counterexample ($$$) # ptr to image list, end state BDD, model { my $imageptr = shift; my $endState = shift; my $M = shift; # model my $T = $M->transition_rel(); # transition relation my $postVarCube = $M->next_state_cube(); # jump out to special-purpose Aiger Model counterexample generation if ( $M->isa("AigerModel") ) { return aiger_counterexample($imageptr, $endState, $M); } elsif ( $M->isa("AbstractAigerModel") || $M->isa("HiddenVarAigerModel")) { return abstract_counterexample($imageptr, $endState, $M); } die "Non-AIGER counterexamples need fixing."; my @statevars = $M->state_vars(); my @images = @$imageptr; my @preimages = (); my @states = (); my $image = pop(@images); $image = $endState * $image; my ($groundState, $state) = pick_state($image, \@statevars); push @states, $groundState; while (@images) { my $image = pop(@images); die "Image is Zero." if ($image == $image->Zero); my $preimage = compute_preimage($state, $M); die "Preimage is inconsistent" if ($preimage == $preimage->Zero); $preimage = $preimage * $image; die "Preimage is inconsistent with image" if ($preimage == $preimage->Zero); my ($groundState, $stateBdd) = pick_state($preimage, \@statevars); push @states, $groundState; push @preimages, $preimage; $state = $stateBdd; } my @revstates = reverse(@states); my @revimages = reverse(@images); return (\@revstates,@revimages); } sub aiger_counterexample ($$$) { # ptr to image list, end state BDD, model my $imageptr = shift; my $endState = shift; my $M = shift; # model my $T = $M->transition_rel(); # transition relation my @inputs = $M->inputVars(); my @latches = $M->latchVars(); my $postVarCube = $M->next_state_cube(); my $inputCube = $M->inputCube; my $out = $M->decode_literal(($M->outputs())[0]); my @images = @$imageptr; my @preimages; my @inputS; my @latchS; my @abstractLatchS; my $image = pop(@images); $image = $endState * $image; my ($groundState, $state) = pick_state($image, \@inputs); push @inputS, $groundState; ($groundState, $state) = pick_state($state, \@latches); push @latchS, $groundState; push @preimages, $state; while (@images) { my $image = pop(@images); die "Image is Zero." if ($image == $image->Zero); # limited state -- need to remove the inputs $state = Exists { $inputCube } $state; my $preimage = compute_preimage($state, $M); die "Preimage is inconsistent" if ($preimage == $preimage->Zero); $preimage = $preimage * $image; die "Preimage is inconsistent with image" if ($preimage == $preimage->Zero); my ($groundState, $stateBdd) = pick_state($preimage, \@inputs); push @inputS, $groundState; ($groundState, $stateBdd) = pick_state($stateBdd, \@latches); push @latchS, $groundState; push @preimages, $stateBdd; $state = $stateBdd; } @inputS = reverse(@inputS); @latchS = reverse(@latchS); @preimages = reverse(@preimages); { my @states; for (my $i = 0; $i <= $#inputS; $i++) { my $inputString = join "", @{$inputS[$i]}; my $latchString = join "", @{$latchS[$i]}; my $outputval = (($out * $preimages[$i]) == $out->Zero) ? 0 : 1; push @states, sprintf "%d\n\tInputs: %s\n\tLatches: %s\n\tOutput: %d\n", $i, $inputString, $latchString, $outputval; } return (\@states, \@preimages); } } sub abstract_counterexample ($$$) { # ptr to image list, end state BDD, model my $imageptr = shift; my $endState = shift; my $M = shift; # model my $groundModel = $M->{groundModel}; my $T = $M->transition_rel(); # transition relation my @inputs = $groundModel->inputVars(); my @latches = $groundModel->latchVars(); my $latchCube = $groundModel->make_cube(@latches); # in order to compute the preimages happily, we need to use the *abstract* # model's inputs, including treating the hidden latches as inputs. my $inputCube = $M->inputCube; my $postVarCube = $M->next_state_cube(); my $out = $M->decode_literal(($M->outputs())[0]); my @images = @$imageptr; my @preimages; my @inputS; my @latchS; my $image = pop(@images); $image = $endState * $image; my ($groundState, $state) = pick_state($image, \@inputs); push @inputS, $groundState; ($groundState, $state) = pick_state($state, \@latches); push @latchS, $groundState; push @preimages, $state; while (@images) { my $image = pop(@images); die "Image is Zero." if ($image == $image->Zero); if ($cautious) { die "Extraneous variables in state structure" unless ( ( $image->Support->LiteralSetIntersection($latchCube) ) == $image->Support ); } # limited state -- need to remove the inputs $state = Exists { $inputCube } $state; my $preimage = compute_preimage($state, $M); die "Preimage is inconsistent" if ($preimage == $preimage->Zero); $preimage = $preimage * $image; die "Preimage is inconsistent with image" if ($preimage == $preimage->Zero); if (! @images) { # we are at the initial state $preimage = $preimage * $groundModel->initial_state(); die "First image is inconsistent with the ground model initial state" if ($preimage == $preimage->Zero); } my ($groundState, $stateBdd) = pick_state($preimage, \@inputs); push @inputS, $groundState; ($groundState, $stateBdd) = pick_state($stateBdd, \@latches); push @latchS, $groundState; push @preimages, $stateBdd; $state = $stateBdd; } @inputS = reverse(@inputS); @latchS = reverse(@latchS); @preimages = reverse(@preimages); { my @states; for (my $i = 0; $i <= $#inputS; $i++) { my $inputString = join "", @{$inputS[$i]}; my $latchString = join "", @{$latchS[$i]}; my $outputval = (($out * $preimages[$i]) == $out->Zero) ? 0 : 1; push @states, sprintf "%d\n\tInputs: %s\n\tLatches: %s\n\tOutput: %d\n", $i, $inputString, $latchString, $outputval; } return (\@states,\@preimages); } } =item print_counterexample ($listptr) Simple helper that prints a sequence of state strings =cut sub print_counterexample (@) { my @states = @_; print "Counterexample:\n"; foreach my $state (@states) { foreach my $x (@$state) { print "$x"; } print "\n"; } } sub nonempty ($) { my $Bdd = shift; my $tmp = ($Bdd == $Bdd->Zero); return ! $tmp; } =item bddnum ($bdd) Debugging utility that prints the node index of C<$bdd> =cut sub bddnum { my $var = shift; return Cudd::NodeReadIndex($var->{'node'}); } =item latch_bdds ($model) Debugging utility that prints the node index of the latches in C<$model>. =cut sub latch_bdds { my $model = shift; my @latches = $model->latchVars(); my @latch_literals = $model->latch_literals(); die "Number of latch variables ($#latches) and latch literals ($#latch_literals) doesn't match" unless $#latches == $#latch_literals; print "Latches of model are:\n"; for (my $i = 0; $i <= $#latches; $i++) { my $ind = bddnum($latches[$i]); print "\tliteral: $latch_literals[$i]\tbdd index: $ind\n"; } return; } sub warn_or_die { if ($debugMode) { warn @_; } else { die @_; } } =item is_subset($lst,$olst) =C<$lst> and =C<$olst> pointers to lists of integers. Boolean; returns true if $lst is a subset of $olst. =cut sub is_subset { my $pos_subset_ptr = shift; my $pos_superset_ptr = shift; my @pos_subset = @{$pos_subset_ptr}; my @pos_superset = @{$pos_superset_ptr}; my $superset = 1; foreach my $x (@pos_subset) { if (! (grep { $_ == $x} @pos_superset) ) { $superset = 0; last; } } return $superset; } =item remove_redundant(@list) Return a new list that contains all of the members of =C<@list> that are not supersets of some other member. =cut sub remove_redundant { my @rows = @_; my @newrows; foreach my $row (@rows) { my $subsumed = 0; foreach my $other (@rows) { if ($row == $other) { next; } elsif (is_subset($other, $row)) { $subsumed =1; last; } } if (! $subsumed) { push @newrows, $row; } } return @newrows; } =item print_ilp(@rowlist) Prints all of the rows in =C<@rowlist>. Each row should be a pointer to a sublist. =cut sub print_ilp { my @rows = @_; print "----------------------------------------\n"; print "Minimized ILP:\n" if $interactive; foreach my $row (@rows) { my $printrow = join(" ", @{$row}); print "$printrow\n"; } print "----------------------------------------\n\n"; return; } =back =cut 1; QCHECK/perl-cegar/ModelChecker.pm~000755 000765 000024 00000104734 12332735011 020061 0ustar00fspedalistaff000000 000000 #!/usr/bin/env perl =head1 Name ModelChecker -- perl utilities for OBDD-based model-checking =head1 Synopsis my $model = Aiger::read_aig_file($ARGV[0]); ModelChecker::model_check($model); or ModelChecker::cegar_model_check($model); =head1 Description Somewhat generic model-checking, based on the L Perl DD library. Only handles reachability model-checking and will not work unless using an AIGER-based model (see L). Offers two options: a simple reachability model checking, C, and a (only semi-implemented) version of the CEGAR counter-example guided abstraction refinement =head2 Functions =over =cut package ModelChecker; require Exporter; @ISA = qw(Exporter); # FIXME: *temporarily* exporting state_gen for unit testing. @EXPORT_OK = qw(model_check cegar_model_check verbose); use Cudd; use warnings; use strict; use Model; use AigerModel; use AbstractAigerModel; use HiddenVarAigerModel; use Array::Utils qw{intersect array_minus}; our $verbose = 0; # throttle output... our $cautious = 1; our $manager; #/* BDD Manager */ our $debugMode = defined &DB::DB; sub compute_image($$;$); # state, model, limiting state (optional) sub compute_preimage ($$); # state, model sub pick_state ($$); # BDD, pointer to variable list sub cegar_model_check ($); # pointer to AigerModel sub model_check ($); # pointer to Model (could be AigerModel) sub check_abs_path ($@); # pointer to ground model, list of images sub refine_abstraction($$$$); # abstract model, deadEnd BDD, image list (ptr) and index of unreachable image sub nonempty($); # is BDD argument nonempty (i.e., != Zero)? sub progress_statevars ($$); sub regress_statevars ($$); sub aiger_counterexample ($$$); # ptr to image list, end state BDD, model sub print_counterexample(@); #helper function sub compute_counterexample ($$$); # ptr to image list, end state BDD, model sub state_gen ($$@); sub verbose ($) { $verbose = shift; } sub model_check ($) { my $model = shift; die "Model not of expected type." unless $model->isa("Model"); my $I = $model->initial_state; # the initial state BDD my $E = $model->target_state; # /* the final state BDD */ # print STDERR "Target state is $E\n"; print STDERR "Making transition relation\n" if $verbose; my $T = $model->transition_rel; # /* the transition relation */ print STDERR "Done making transition relation\n" if $verbose; my $R; # reachable states BDD my $Core; # "core" BDD of latch values used to # generate successor states. my $image; my @images; # used to compute the counterexample... print STDERR "Preparing for model-checking.\n" if $verbose; $manager = $model->manager(); #/* enable dynamic reordering */ $manager->EnableDyn(); # This fails if $E->Not() is a tautology. [2013/10/15:rpg] if ($E == $manager->BddOne) { print "target state is vacuously true.\n"; exit 0; } elsif ($E->Not() == $manager->BddOne) { print "target state is vacuously false.\n"; exit 0; } if (( $I->Or($E->Not()) ) == $manager->BddOne) { print STDERR "Negated target state is:\n"; $E->Not()->Print(1, 3); print STDERR "Initial state is:\n"; $I->Print(1, 3); if ($I->Equal($E->Not()) ) { # this should be true... print "Initial state is the negation of the target state\n"; } elsif ($I->Equal($E) ) { print "Initial state is the target state\n"; } my @vars = $model->now_vars(); my ($stateref, $bdd) = pick_state($I, \@vars); my @state = @{$stateref}; print "Pick state returns: @state\n"; return 1; } # print STDERR "Building cube of current state variables\n" if $verbose; # #/* Cube of the current state variables, needed by bddAndAbstract */ # my $cube = $model->this_state_cube(); # print STDERR "initialized current state variable cube.\n" if $verbose; # print STDERR "Building cube of next state variables\n" if $verbose; # my $nsCube = $model->next_state_cube(); # print STDERR "initialized next state variable cube.\n" if $verbose; my $num_steps = 0; my $found = 0; # R contains the states reached so far, initialized to I $R = $I; push @images, $R; # get the initial state onto the images list print "Starting fixed point computation.\n" if $verbose; # $DB::single = 1; #/* Fixed point computation */ while (1) { my $tmp1; my $tmp2; my $tmp3; my $image; #/* check if we reached the goal state */ print "Checking for goal\n" if $verbose; if ( ($E * $R) != $E->Zero ) #(($E->Not + $R) == $E->One) { print "Goal reached\n"; $found = 1; #/* goal reached */ last; } #/* compute the successors of the current state */ print "Computing successors\n" if $verbose; $image = compute_image($R,$model); $num_steps ++; #/* check if we reached a new state */ #/* Note: Fixed point check, easy with BDDs as they are canonical */ print "Checking for new state\n" if $verbose; $tmp2 = $image->Not() + $R; if ($tmp2 == $manager->BddOne) { print "Reached fixpoint after $num_steps steps\n" if $verbose; last; #/* no new state reached */ } #/* add the new states to the reached set */ $tmp3 = $image + $R; push @images, $image; $R = $tmp3; } my ($statesptr,$bddstateptr); # for catching the counterexample return values. if ($found) { printf("Goal Reached in %d steps\n",$num_steps); { # make sure the final state of the images hits the goal my $i = $#images; $images[$i] = $images[$i] * $E; } if ($num_steps > 0) { my @imagecopy = @images; ($statesptr,$bddstateptr) = compute_counterexample(\@imagecopy, $E, $model); print "Counterexample:\n"; foreach my $state (@$statesptr) { print $state; } } } else { printf("Goal not reached\n"); } return $found, \@images; } =item invert_image_vector($model, $imageListPtr) Take the list of images, made by progression from the initial state (which should be =C<${$imageListPtr}[0]>), generate and return a new counterexample trace by regressing the end state (which must satisfy =C<$model->target_state()>) back to the initial state. This fixes a problem where the original trace is not limited to states that can eventually lead to the target state. =cut sub invert_image_vector ($$) { my $model = shift; my $imagelistPtr = shift; my @imagelist = @{$imagelistPtr}; my @newimages; my @latches = $model->latchVars(); # for debugging... my $latchCube = $model->make_cube(@latches); my $inputCube = $model->inputCube(); my @groundStates; my $image = pop(@imagelist); my ($groundState, $state) = pick_state($image, \@latches); push @newimages, $state; push @groundStates, $groundState; while (@imagelist) { my $image = pop(@imagelist); die "Image is Zero." if ($image == $image->Zero); # note that the image structure may have some extra variables in the case # where it's the initial state... if ($cautious) { die "Extraneous variables in state structure" unless ( ( $state->Support->LiteralSetIntersection($latchCube) ) == $state->Support ); } my $preimage = compute_preimage($state, $model); die "Preimage is inconsistent" if ($preimage == $preimage->Zero); $preimage = $preimage * $image; die "Preimage is inconsistent with image" if ($preimage == $preimage->Zero); if (! @imagelist) { # we are at the initial state $preimage = $preimage * $model->initial_state(); die "First image is inconsistent with the ground model initial state" if ($preimage * $model->{groundModel}->initial_state == $preimage->Zero); } my ($groundState, $stateBdd) = pick_state($preimage, \@latches); $stateBdd = Exists {$inputCube} $stateBdd; push @newimages, $stateBdd; push @groundStates, $groundState; $state = $stateBdd; } if ($verbose > 0) { print "Abstract counterexample:\n"; foreach my $groundState (reverse(@groundStates)) { my $latchString = join "", @{$groundState}; printf "\t%s\n", $latchString; } } return reverse(@newimages); } sub cegar_model_check ($) { my $model = shift; # pointer to AigerModel die "cegar_model_check only implemented for AigerModels" unless $model->isa("AigerModel"); my $abs = initial_abstraction($model); my $found; my @images; my $imgptr; while (1) { { my @hidden = @{$abs->{hiddenLits}}; print STDERR "Checking abstract model, hidden literals are: @hidden\n"; if ( ! @hidden ) { print STDERR "Degenerate case of CEGAR model checking: no hidden literals.\n"; return model_check($model); } } ($found, $imgptr) = model_check($abs); if (! $found) { print "No abstract path to goal state: circuit is safe.\n"; last; } else { @images = invert_image_vector($abs,$imgptr); # the images above are a raw sequence of images from the forward # reachability search. We will reformulate them to get an abstract # counterexample (where only the visible variables are grounded). That # will drive our refinement process. my ($invalid, $deadEnd) = check_abs_path($model,@images); if ( !$invalid ) { print "Abstract counterexample is valid.\n"; last; } else { print "Abstract counterexample is invalid at step $invalid.\n"; $abs = refine_abstraction($abs, $deadEnd, \@images, $invalid); } } } return $found; } =item abstract_images($abstractModel, @imageList) Return a new list of images (BDDs), corresponding to c<@imageList>, but abstracted according to the abstract model. =cut # FIXME: rewrite this to use abstract_state. Also modify AbstractAigerModel so # that the hiddenCube is memoized. sub abstract_images ($@) { my ($absModel, @images) = @_; my @retval; my $hiddenCube = $absModel->hiddenCube(); foreach my $img (@images) { my $new = Exists { $hiddenCube } $img; push @retval, $new; } return @retval; } =item abstract_images($abstractModel, $BDD) Return a new state (BDD), corresponding to c<$BDD>, but abstracted according to the abstract model, c<$abstractModel>. =cut sub abstract_state ($$) { my ($absModel, $bdd) = @_; my $hiddenCube = $absModel->hiddenCube(); return Exists {$hiddenCube} $bdd; } sub initial_abstraction ($) { my $model = shift; my @show = $model->init_latches_to_show(); my $abs = new AbstractAigerModel({model=>$model,show=>\@show}); # my $abs = new HiddenVarAigerModel({model=>$model,show=>\@show}); return $abs; } =item check_abs_path($M, @images) Takes a path of I images, and the I model, C<$M> underlying them and checks to see if the path of images is a valid counterexample for the ground model. If it is I valid, returns two values: =over =item 1. The index of the bad state (this should always be greater than or equal to one). =item 2. The BDD for the last valid ground state (this will be a concrete state corresponding to the abstract state immediately prior to the index returned. =back If the counterexample is valid, this subroutine will return zero. =cut sub check_abs_path ($@) { my $groundModel = shift; my @images = @_; my $S; # CUDD BDD my $Sprev; # $S = h-1($s1) * $groundModel->initial_state(); $S = $groundModel->initial_state(); $S = $S * $images[0]; die "Invalid initial state." unless nonempty($S); # j starts at 1 (incremented at top of loop) because the zeroth image has # already been used my $j = 0; while (nonempty($S) && $j < $#images) { $j++; $Sprev = $S; $S = compute_image($S, $groundModel); $S = $S * $images[$j]; } if (nonempty($S) ) { return 0; } else { return $j, $Sprev; } } =item refine_abstraction($absModel, $deadEnd, $imageptr, $i) The arguments should be: =over =item the abstracted model object, =item the dead end state computed by "playing back" the abstract counterexample in the ground model, =item a pointer to the list of images in the abstract reachability graph to the target state and =item the index in the images of the unreachable state (one past the dead end state). =back as a side-effect, prints an ILP. Returns a new refined (but still, in general, abstract) model. =cut # <> sub refine_abstraction($$$$) { # abstract model, deadEnd BDD, images list and index of unreachable state my $absModel = shift; my $deadEnd = shift; # *concrete* dead end state in faulty counterexample my $imageptr = shift; my $unreachableIndex = shift; my @images = @$imageptr; # a list of abstract states, the (faulty) abstract counterexample my $newModel; my $prefilter; my $groundModel = $absModel->{groundModel}; # $bad == ground states that are in the pre-image of the unreachable state my $absUnreachable = $images[$unreachableIndex]; if ($absModel->isa("AbstractAigerModel")) { # $absUnreachable = Exists {$absModel->hiddenCube} $absUnreachable; $absUnreachable = Exists {$groundModel->inputCube} $absUnreachable; } my $bad = compute_preimage($absUnreachable, $groundModel); die "No preimage of unreachable state." if $bad == $bad->Zero; $bad = Exists {$groundModel->inputCube} $bad; $prefilter = $images[$unreachableIndex-1]; if ($absModel->isa("AbstractAigerModel")) { $prefilter = Exists {$absModel->hiddenCube} $prefilter; $prefilter = Exists {$absModel->inputCube} $prefilter; } $bad = $bad * $prefilter; if ($bad == $bad->Zero) { $DB::single=1; } die "No bad states." if $bad == $bad->Zero; die "Dead End states and bad states are not mutually exclusive" unless ($bad * $deadEnd) == $bad->Zero; # for now, just dump an ILP: my @hidden ; my @hlits; # need to remove irrelevant literals... # FIXME: this code is ugly because I butchered it in -- should be pulled out { my $sos = $deadEnd->Support()->LiteralSetIntersection($bad->Support()); my @vars = $absModel->hidden_vars(); my @lits = @{$absModel->{hiddenLits}}; for (my $i = 0; $i <= $#vars; $i++) { # var is in the set of support if ( $vars[$i]->LiteralSetIntersection($sos) == $vars[$i] ) { push @hidden, $vars[$i]; push @hlits, $lits[$i]; } } } my $deGen = state_gen($deadEnd, $groundModel, @hidden); my $deState; my @rows; print "ILP is:\n"; my $showLiteral; while (defined($deState=$deGen->())) { print STDERR "Comparing dead end state @{$deState}\n" if $verbose > 2; my $badGen = state_gen($bad, $groundModel, @hidden); my $badState; while (defined($badState=$badGen->())) { print STDERR "\tcomparing to bad state @{$badState}\n" if $verbose > 2; my @row; for (my $i = 0; $i <= $#hlits; $i++) { if (${$deState}[$i] != ${$badState}[$i]) { # print "$hlits[$i] "; push @row, $hlits[$i]; } } if (!@row) { warn "No difference between states @{$deState} and @{$badState}" unless @row; next; } print STDERR "\tNew row @row\n" if $verbose > 2; { my $found = 0; foreach my $other (@rows) { if ( is_subset($other,\@row) ){ $found = 1; last; } } if (! $found) { push @rows, \@row; print "@row\n"; } else { print STDERR "Row @row subsumed by previous entry.\n" if $verbose > 2 } } } } @rows = remove_redundant(@rows); print_ilp(@rows); my @common = every_member(@rows); if (@common) { $showLiteral = $common[0]; die "Error picking an intersection literal" unless $showLiteral; print STDERR "Splitting on literal $showLiteral\n" if $verbose; $newModel = simple_refinement($absModel,$showLiteral); } else { print STDERR "No common element in ILP. Enter literals to split on.\n"; my $done = 0; my @fields; while (! $done) { my $split; chomp ($split = ); @fields = split /[\s,]+/, $split; print STDERR "Will split on:\n"; foreach my $field (@fields) { print STDERR "$field "; } print "\nOK? "; my $ans; chomp ($ans = ); $done = ($ans eq "y") || ($ans eq "Y"); } print STDERR "Splitting on @fields\n" if $verbose; $newModel = $absModel; foreach my $field (@fields) { $newModel = simple_refinement($newModel, $field); } } return $newModel; } =item every_member Take a list of lists (list of list pointers) as argument. Return a list of elements that appear in every list. =cut sub every_member (@) { my @list = @_; my @first_list = @{$list[0]}; my @rest = @list[1..$#list]; my @retval = @first_list; map { @retval = intersect(@retval, @{$_}); } @rest; return @retval; } =item simple_refinement($oldAbsModel,$literalToShow) Make and return a simple refined model derived from C<$oldAbsModel> by un-hiding C<$literalToShow>. =cut sub simple_refinement ($$) { my ($oldAbsModel,$literalToShow) = @_; my @shown = @{$oldAbsModel->{shownLits}}; push @shown,$literalToShow; @shown = sort {$a <=> $b} @shown; my $newModel = new AbstractAigerModel({model=>$oldAbsModel->{groundModel}, show=>\@shown}); # my $newModel = new HiddenVarAigerModel({model=>$oldAbsModel->{groundModel}, # show=>\@shown}); die "Showing not working" if $newModel->is_hidden($literalToShow); return $newModel; } =item all_states($BDD, $Model, @variables) Use the state generator (created by L) to compute all the assignments to C<@variables> consistent with c<$BDD>. =cut sub all_states ($$@) { my ($bdd,$model, @vars) = @_; my $gen = state_gen($bdd,$model,@vars); my @res; my $s; while (defined($s = $gen->())) { push @res,$s; } return @res; } =item state_gen($BDD, $Model, @variables) Return a generator for states from a BDD, given variables. =cut sub state_gen ($$@) { my ($bdd, $model, @vars) = @_; # my @vars; # foreach my $lit (@lits) { # push @vars, $model->decode_literal($lit); # } my @arr = (0) x ($#vars + 1); my $done = 0; return sub { return undef if ($done); my $found = 0; my $asgn; my $retval; while (1) { ($found, $asgn) = next_state($model, $bdd, \@vars, \@arr); @$retval = @$asgn; # print "Found value is $found for @$asgn\n"; $done = incr_state(\@arr); # prepare for next # print "Done value is $done\n"; last if ($found); last if ($done); } if ($found) { # print "Found so returning @$retval\n"; return $retval; } elsif ($done) { return undef; } } } =item next_state($model, $bdd, $varptr, $valptr) Helper function for the state_gen iterator. Should not be called directly. =C<$varptr> is a pointer to a list of variables, and =C<$valptr> a pointer to a list of variable values (1 or zero). =cut sub next_state ($$$$) { my ($model, $bdd, $varptr, $valptr) = @_; my $found = 1; my @vars = @$varptr; my @vals = @$valptr; for (my $i = 0; $i <= $#vars; $i++) { # print "checking var value $i\n"; if ($vals[$i] == 0) { $bdd = $bdd * !$vars[$i]; } else { $bdd = $bdd * $vars[$i]; } if ($bdd == $bdd->Zero) { $found = 0; last; } } return $found, $valptr; } # side effects to increment the binary vector in its # (pointer) argument. Returns a boolean indicating whether # the array has overflowed. sub incr_state($) { my $arr = shift; my @array = @$arr; my $carry = 1; for (my $i = 0; $i <= $#array; $i++) { my $tmp = ${$arr}[$i] ^ $carry; $carry = ${$arr}[$i] & $carry; ${$arr}[$i] = $tmp; } return $carry; } # /* */ =item compute_image($R, $M) Given a set of states, C<$R> and a Model, C<$M>, returns the BDD for the states that can be reached in one step from C<$R> following the transition relation of C<$M>. =cut sub compute_image ($$;$) # $R - reachable states, $M - model, optional limiting state { my ($R, $M, $limit) = @_; # FIXME: in AIGER mode, there may be this state variables that need to be # removed when progressing the state that are NOT latch variables (so don't # get rewritten). Fix by using class-specific progression methods? my $cube = $M->this_state_cube(); my $T = $M->transition_rel(); my $result; # /* the following Cudd function computes the conjunction of R and T; and quantifies out the variables # in cube ( the current state variables ) */ print "Calling AndExists\n" if $verbose >= 2; $result = Exists { $cube } $R * $T; # $result = $cube->AndExists($R, $T); <- couldn't get this to work print "Done with AndExists\n" if $verbose >= 2; if (defined $limit) { # FIXME: think this may be applying limiting to the wrong state -- it's a mess. warn_or_die("Limiting logic may not yet work."); $result = $result * $limit; } # FIXME: big heap of debugging code. Need to remove it eventually. # { # my $supp = $nextCore->Support(); # if ( ! ($nsCube == $supp ) ) { # my $inputCube = $M->inputCube(); # my $intersection = $inputCube->LiteralSetIntersection($supp); # if (! $intersection->Equal($supp->One)) { # # Cudd::BDD::Dot([$inputCube]); # # Cudd::BDD::Dot([$supp]); # # Cudd::BDD::Dot([$intersection]); # die "There's a non-empty intersection between the support and the set of inputs."; # } # print "Next State Cube:\n"; # Cudd::BDD::Dot([$nsCube]); # print "Next core support cube:\n"; # Cudd::BDD::Dot([$supp]); # die "Support of the AndExists is not the same as the next state variables.\n"; # } # } die "Result not a BDD" unless $M->is_bdd($result); print "Renaming next state variables\n" if $verbose >= 2; # /* rename the next state variables to the current state variables */ $result = progress_statevars($M, $result); print "Done renaming next state variables\n" if $verbose >=2; return $result; } =item progress_statevars ($Model, $BDD) Replace the next state variables in C<$BDD> with current state variables, according to C<$Model>. Returns a new BDD. In order for this to be correctly used, the next statevars should not already be present. =cut # <> sub progress_statevars ($$) { my ($M, $Bdd) = @_; my @statevars = $M->state_vars(); my @next_statevars = $M->next_state_vars(); if ($cautious) { if ($Bdd->Support()->LiteralSetIntersection($M->make_cube(@statevars)) != $Bdd->One) { die "Calling progress_statevars on an unprepared state -- current statevars should be quantified away."; } } die "Number of new and old state variables disagree in cardinality." unless $#statevars == $#next_statevars; for (my $i = 0; $i <= $#statevars; $i++) { # print "$i\n"; die "Type error" unless $M->is_bdd($next_statevars[$i]) && $M->is_bdd($statevars[$i]); # $next_statevars[$i]->Print(1,2); # $statevars[$i]->Print(1,2); my $tmp1 = $Bdd->Compose($next_statevars[$i], $statevars[$i]); $Bdd = $tmp1; } return $Bdd; } =item regress_statevars ($Model, $BDD) The opposite of =L, here we replace the current state variables in C<$BDD> with next state variables, according to C<$Model>. Returns a new BDD. =cut # <> sub regress_statevars ($$) { my ($M, $Bdd) = @_; my @statevars = $M->state_vars(); my @next_statevars = $M->next_state_vars(); if ($cautious) { if ($Bdd->Support()->LiteralSetIntersection($M->make_cube(@next_statevars)) != $Bdd->One) { die "Calling regress_statevars on an unprepared state -- next state variables should be quantified away."; } } die "Number of new and old state variables disagree in cardinality." unless $#statevars == $#next_statevars; for (my $i = 0; $i <= $#statevars; $i++) { # print "$i\n"; die "Type error" unless $M->is_bdd($next_statevars[$i]) && $M->is_bdd($statevars[$i]); # $next_statevars[$i]->Print(1,2); # $statevars[$i]->Print(1,2); my $tmp1 = $Bdd->Compose($statevars[$i],$next_statevars[$i]); $Bdd = $tmp1; } return $Bdd; } =item compute_preimage($Bdd, $Model) Return a new BDD that represents the preimage of =C<$Bdd> according to =C<$Model>. The resulting BDD will be a boolean function of current state variables (e.g., latches), and inputs. This is appropriate for computing a counterexample, but if it were to be used in computing backwards reachability, probably the inputs should be quantified away before using the result. =cut sub compute_preimage ($$) { # state, Model my $state = shift; my $M = shift; my $T = $M->transition_rel(); my $postVarCube = $M->next_state_cube(); if ($cautious) { die "Attempting to compute the preimage of a state including excess variables." unless ( $state->Support->LiteralSetIntersection($M->make_cube($M->state_vars())) == $state->Support() ); # we should have only state variables here -- not even extended state # variables (e.g., with inputs) } # successor state with the current state variables turned into next # state variables where appropriate my $succ_state = regress_statevars($M, $state); # the following looks like voodoo programming; removing this call as unnecessary. [2014/01/09:rpg] # # now we remove all the remaining state variables # $succ_state = Exists { $M->this_state_cube } $succ_state; # now we should have a bunch of post-state variables. # Regress them over the transition relation and return the # resulting state. my $result = Exists { $postVarCube } $succ_state * $T; return $result; } =item pick_state($BDD, $varlistPtr) Return two values: the first is a pointer to a list of boolean values indicating the assignment of values to the variables in the variable list. The second is a BDD representing this assignment in the context of $BDD. =cut sub pick_state ($$) { my $bdd = shift; my $vars = shift; my @vars = @$vars; my @state = (); my $zero = $bdd->Zero; foreach my $var (@vars) { if ( ( $bdd * $var) != $zero) { $bdd = $bdd * $var; push @state, 1; } else { $bdd = $bdd * !$var; push @state, 0; } } return (\@state, $bdd); } sub compute_counterexample ($$$) # ptr to image list, end state BDD, model { my $imageptr = shift; my $endState = shift; my $M = shift; # model my $T = $M->transition_rel(); # transition relation my $postVarCube = $M->next_state_cube(); # jump out to special-purpose Aiger Model counterexample generation if ( $M->isa("AigerModel") ) { return aiger_counterexample($imageptr, $endState, $M); } elsif ( $M->isa("AbstractAigerModel") || $M->isa("HiddenVarAigerModel")) { return abstract_counterexample($imageptr, $endState, $M); } die "Non-AIGER counterexamples need fixing."; my @statevars = $M->state_vars(); my @images = @$imageptr; my @preimages = (); my @states = (); my $image = pop(@images); $image = $endState * $image; my ($groundState, $state) = pick_state($image, \@statevars); push @states, $groundState; while (@images) { my $image = pop(@images); die "Image is Zero." if ($image == $image->Zero); my $preimage = compute_preimage($state, $M); die "Preimage is inconsistent" if ($preimage == $preimage->Zero); $preimage = $preimage * $image; die "Preimage is inconsistent with image" if ($preimage == $preimage->Zero); my ($groundState, $stateBdd) = pick_state($preimage, \@statevars); push @states, $groundState; push @preimages, $preimage; $state = $stateBdd; } my @revstates = reverse(@states); my @revimages = reverse(@images); return (\@revstates,@revimages); } sub aiger_counterexample ($$$) { # ptr to image list, end state BDD, model my $imageptr = shift; my $endState = shift; my $M = shift; # model my $T = $M->transition_rel(); # transition relation my @inputs = $M->inputVars(); my @latches = $M->latchVars(); my $postVarCube = $M->next_state_cube(); my $inputCube = $M->inputCube; my $out = $M->decode_literal(($M->outputs())[0]); my @images = @$imageptr; my @preimages; my @inputS; my @latchS; my @abstractLatchS; my $image = pop(@images); $image = $endState * $image; my ($groundState, $state) = pick_state($image, \@inputs); push @inputS, $groundState; ($groundState, $state) = pick_state($state, \@latches); push @latchS, $groundState; push @preimages, $state; while (@images) { my $image = pop(@images); die "Image is Zero." if ($image == $image->Zero); # limited state -- need to remove the inputs $state = Exists { $inputCube } $state; my $preimage = compute_preimage($state, $M); die "Preimage is inconsistent" if ($preimage == $preimage->Zero); $preimage = $preimage * $image; die "Preimage is inconsistent with image" if ($preimage == $preimage->Zero); my ($groundState, $stateBdd) = pick_state($preimage, \@inputs); push @inputS, $groundState; ($groundState, $stateBdd) = pick_state($stateBdd, \@latches); push @latchS, $groundState; push @preimages, $stateBdd; $state = $stateBdd; } @inputS = reverse(@inputS); @latchS = reverse(@latchS); @preimages = reverse(@preimages); { my @states; for (my $i = 0; $i <= $#inputS; $i++) { my $inputString = join "", @{$inputS[$i]}; my $latchString = join "", @{$latchS[$i]}; my $outputval = (($out * $preimages[$i]) == $out->Zero) ? 0 : 1; push @states, sprintf "%d\n\tInputs: %s\n\tLatches: %s\n\tOutput: %d\n", $i, $inputString, $latchString, $outputval; } return (\@states, \@preimages); } } sub abstract_counterexample ($$$) { # ptr to image list, end state BDD, model my $imageptr = shift; my $endState = shift; my $M = shift; # model my $groundModel = $M->{groundModel}; my $T = $M->transition_rel(); # transition relation my @inputs = $groundModel->inputVars(); my @latches = $groundModel->latchVars(); my $latchCube = $groundModel->make_cube(@latches); # in order to compute the preimages happily, we need to use the *abstract* # model's inputs, including treating the hidden latches as inputs. my $inputCube = $M->inputCube; my $postVarCube = $M->next_state_cube(); my $out = $M->decode_literal(($M->outputs())[0]); my @images = @$imageptr; my @preimages; my @inputS; my @latchS; my $image = pop(@images); $image = $endState * $image; my ($groundState, $state) = pick_state($image, \@inputs); push @inputS, $groundState; ($groundState, $state) = pick_state($state, \@latches); push @latchS, $groundState; push @preimages, $state; while (@images) { my $image = pop(@images); die "Image is Zero." if ($image == $image->Zero); if ($cautious) { die "Extraneous variables in state structure" unless ( ( $image->Support->LiteralSetIntersection($latchCube) ) == $image->Support ); } # limited state -- need to remove the inputs $state = Exists { $inputCube } $state; my $preimage = compute_preimage($state, $M); die "Preimage is inconsistent" if ($preimage == $preimage->Zero); $preimage = $preimage * $image; die "Preimage is inconsistent with image" if ($preimage == $preimage->Zero); if (! @images) { # we are at the initial state $preimage = $preimage * $groundModel->initial_state(); die "First image is inconsistent with the ground model initial state" if ($preimage == $preimage->Zero); } my ($groundState, $stateBdd) = pick_state($preimage, \@inputs); push @inputS, $groundState; ($groundState, $stateBdd) = pick_state($stateBdd, \@latches); push @latchS, $groundState; push @preimages, $stateBdd; $state = $stateBdd; } @inputS = reverse(@inputS); @latchS = reverse(@latchS); @preimages = reverse(@preimages); { my @states; for (my $i = 0; $i <= $#inputS; $i++) { my $inputString = join "", @{$inputS[$i]}; my $latchString = join "", @{$latchS[$i]}; my $outputval = (($out * $preimages[$i]) == $out->Zero) ? 0 : 1; push @states, sprintf "%d\n\tInputs: %s\n\tLatches: %s\n\tOutput: %d\n", $i, $inputString, $latchString, $outputval; } return (\@states,\@preimages); } } =item print_counterexample ($listptr) Simple helper that prints a sequence of state strings =cut sub print_counterexample (@) { my @states = @_; print "Counterexample:\n"; foreach my $state (@states) { foreach my $x (@$state) { print "$x"; } print "\n"; } } sub nonempty ($) { my $Bdd = shift; my $tmp = ($Bdd == $Bdd->Zero); return ! $tmp; } =item bddnum ($bdd) Debugging utility that prints the node index of C<$bdd> =cut sub bddnum { my $var = shift; return Cudd::NodeReadIndex($var->{'node'}); } =item latch_bdds ($model) Debugging utility that prints the node index of the latches in C<$model>. =cut sub latch_bdds { my $model = shift; my @latches = $model->latchVars(); my @latch_literals = $model->latch_literals(); die "Number of latch variables ($#latches) and latch literals ($#latch_literals) doesn't match" unless $#latches == $#latch_literals; print "Latches of model are:\n"; for (my $i = 0; $i <= $#latches; $i++) { my $ind = bddnum($latches[$i]); print "\tliteral: $latch_literals[$i]\tbdd index: $ind\n"; } return; } sub warn_or_die { if ($debugMode) { warn @_; } else { die @_; } } =item is_subset($lst,$olst) =C<$lst> and =C<$olst> pointers to lists of integers. Boolean; returns true if $lst is a subset of $olst. =cut sub is_subset { my $pos_subset_ptr = shift; my $pos_superset_ptr = shift; my @pos_subset = @{$pos_subset_ptr}; my @pos_superset = @{$pos_superset_ptr}; my $superset = 1; foreach my $x (@pos_subset) { if (! (grep { $_ == $x} @pos_superset) ) { $superset = 0; last; } } return $superset; } =item remove_redundant(@list) Return a new list that contains all of the members of =C<@list> that are not supersets of some other member. =cut sub remove_redundant { my @rows = @_; my @newrows; foreach my $row (@rows) { my $subsumed = 0; foreach my $other (@rows) { if ($row == $other) { next; } elsif (is_subset($other, $row)) { $subsumed =1; last; } } if (! $subsumed) { push @newrows, $row; } } return @newrows; } =item print_ilp(@rowlist) Prints all of the rows in =C<@rowlist>. Each row should be a pointer to a sublist. =cut sub print_ilp { my @rows = @_; print "\n----------------------------------------\nMinimized ILP:\n"; foreach my $row (@rows) { my $printrow = join(" ", @{$row}); print "$printrow\n"; } print "----------------------------------------\n\n"; return; } =back =cut 1; QCHECK/perl-cegar/simple-unsolvable.aag000644 000765 000024 00000000176 12332735011 021103 0ustar00fspedalistaff000000 000000 aag 2 0 1 1 1 2 3 4 4 2 3 c Simple example that should never reach output = true, because the AND gate's output is always 0. QCHECK/perl-cegar/simple.aag000644 000765 000024 00000000117 12332735011 016726 0ustar00fspedalistaff000000 000000 aag 2 0 1 1 1 2 3 4 4 2 2 c Simple example that should reach fail in one step. QCHECK/perl-cegar/solver-stub.pl000755 000765 000024 00000001121 12332735011 017604 0ustar00fspedalistaff000000 000000 #!/usr/bin/env perl # This is a cheesy stub for the solver. It just reads an ILP and returns the first variable index it # reads. But it shows the pattern: # open the command line argument file for input open FILE, $ARGV[0]; print STDERR "Solver stub read:\n"; my $spliton; # read the problem from the input file while () { if (m|(\d+)|) { $spliton = $1; } print STDERR $_; } print STDERR "Splitting on $spliton\n"; close FILE; # print the value(s) you want to split on on a single line of space-separated # digits, terminated with a newline. print "$spliton\n"; exit 0; QCHECK/perl-cegar/state_gen_test.pl000644 000765 000024 00000001526 12332735011 020335 0ustar00fspedalistaff000000 000000 #! /usr/bin/env perl # Test reading and solving models formulated using AIGER use Aiger; use AigerModel; use Cudd; use ModelChecker; use strict; use warnings; use Carp; $SIG{ __DIE__ } = sub { Carp::confess( @_ ) }; my $model = Aiger::read_aig_file("/Users/rpg/src/aiger-1.9.4/examples/counter.aig"); # print "Model inputs: "; # print $model->inputs; # print "\n"; # print "Model outputs: "; # print $model->outputs; # print "\n"; # print "Model latches: "; # print $model->latches; # print "\n"; # print "Model and-gates: "; # print $model->andGates; # print "\n"; #exit 0; print "Done reading file and building model.\n"; our $bdd = $model->decode_literal(4) * $model->decode_literal(8); our $cls = ModelChecker::state_gen($bdd, $model, $model->latchVars()); $DB::single=1; our $foo; while (defined ($foo = $cls->())) { print "@$foo\n"; } QCHECK/aiger-model/aiger-model.asd000644 000765 000024 00000001050 12332735323 020010 0ustar00fspedalistaff000000 000000 ;;;; aiger-model.asd (asdf:defsystem #:aiger-model :serial t :description "Design AIGER format models with a lispy syntax" :author "Robert P. Goldman " :license "LLGPL" :depends-on (:iterate) :components ((:file "package") (:file "aiger-model"))) (asdf:defsystem #:aiger-model/tests :serial t :description "Design AIGER format models with a lispy syntax" :author "Robert P. Goldman " :license "LLGPL" :depends-on (:aiger-model :fiveam) :components ((:file "tests"))) QCHECK/aiger-model/aiger-model.lisp000644 000765 000024 00000036542 12332735323 020226 0ustar00fspedalistaff000000 000000 ;;;; aiger-model.lisp (in-package #:aiger-model) #| ;;; Syntax for AIGER models: (model ) ::= form+
::= (input ) | (latch ) | (output ) | (and ) ::= | (not ) | T | F ::= + ::= + ::= | ( ) ::= ;;; We can introduce new blocks as follows: (defblock name (:params :outputs :locals ) ) ;;; Params may be referenced in the block's body, but may not be defined there. ;;; I.e., they may appear in the next val spec for a latch, or as one of the ;;; arguments of an and gate, but cannot appear on the LHS of any expression. ;;; The outputs *must* be defined in the block's body. ;;; use blocks as follows: ( [name] (( )*) (( )*)) ;;; The semantics would involve the following operations: ;;; 1. Take all the local names and standardize them: translate to new names ;;; that refer to the name of the block instance, either set by the caller or ;;; automatically generated. ;;; 2. Take all the instances of the param names and replace them with the ;;; names from the caller. ;;; 3. Take the output names, standardize them, and then make entries in the ;;; surrounding program's table that are aliases for the output names. ;;; Need to be sure that this procedure can be done recursively. The problem ;;; with this is the output names. We need the block expansion program to ;;; return a value that is a name table. |# (defmacro num-args (form n) `(unless (= (length ,form) (1+ ,n)) (error "Form ~a should have ~d arguments." ,form ,n))) ;;;--------------------------------------------------------------------------- ;;; Interface functions ;;;--------------------------------------------------------------------------- (defun translate-from-command-line (argv) (handler-bind ((error #'(lambda (e) (format t "Exiting with error: ~a" e) (sb-ext:exit :code 2)))) (case (length argv) ((2 3) (let ((outfile (apply #'translate-model-file (rest argv)))) (format t "Wrote aag model to ~a~%" (namestring outfile)))) (otherwise (format t "Invalid number of arguments, ~d" (length argv)) (sb-ext:exit :code 1)))) (sb-ext:exit :code 0) ) (defun translate-model-file (file &optional outfile) (let* ((model (read-model-file file)) (outfile (if outfile outfile (merge-pathnames (make-pathname :type "aag") file)))) (with-open-file (str outfile :direction :output :if-exists :supersede) (translate-model model :stream str)) outfile)) (defun translate-model (model &key (stream t)) (multiple-value-bind (block-defs new-model) (cache-block-defs model) (multiple-value-bind (expanded-model symbol-table) (expand-block-defs new-model block-defs) (translate-basic-model expanded-model :stream stream :symbol-table symbol-table)))) ;;;--------------------------------------------------------------------------- ;;; End of interface functions ;;;--------------------------------------------------------------------------- ;;; FIXME: problem here is that recursive invocation doesn't behave properly ;;; with negation... (defun translate-literal (lit name-table) (cond ((and (listp lit) (eq (car lit) 'not)) (num-args lit 1) (negate (translate-literal (second lit) name-table))) ((symbolp lit) (let ((val (gethash lit name-table))) (cond ((numberp val) val) ((null val) (error "Undefined name ~a" lit)) ;; recursive definition (t (translate-literal val name-table))))) (t (error "Ill-formed literal: ~a" lit)))) (defun negate (x) (cond ((oddp x) (1- x)) ((evenp x) (1+ x)) (t (error 'type-error :datum x :expected-type 'integer)))) (defun cache-block-defs (model) "Take the defblock forms out of model and return two values: 1. The cache of defblocks and 2. The model with the defblocks removed." (let (block-defs blocks) (iter (for form in (cddr model)) (when (eq (car form) 'defblock) (push (parse-block form) block-defs) (push form blocks))) (let ((new-body (remove-if #'(lambda (x) (member x blocks)) (cddr model)))) (values block-defs `(model ,(second model) ,@new-body))))) (defstruct (blockdef (:type list) :named) name params outputs locals body ) (defun parse-block (form) (destructuring-bind (keyword name param-block &body body) form (assert (eq keyword 'defblock)) (multiple-value-bind (params outputs locals) (parse-block-params param-block) (make-blockdef :name name :params params :outputs outputs :locals locals :body body)))) (defun expand-block-defs (model block-defs) (multiple-value-bind (expansion table) (expand-blocks-as-needed (cddr model) block-defs) (values `(model ,(second model) ,@expansion) table))) (defun expand-blocks-as-needed (forms blockdefs &optional table) (flet ((add-to-table (table-entries) (setf table (append table table-entries))) (block-name-p (name defs) (member name defs :key #'blockdef-name))) (let ((expansion (iter (for form in forms) (case (car form) ((input latch output and) (appending (list form))) ; handle later (otherwise (cond ((block-name-p (car form) blockdefs) (multiple-value-bind (expansion table-entries) ;; standardize the name here... (expand-block (standardize-form form) blockdefs) (add-to-table table-entries) ;; recursively expand contained blocks... (multiple-value-bind (new-exp new-table) (expand-blocks-as-needed expansion blockdefs table) (setf table new-table) (appending new-exp)))) (t (error "unknown block: ~a" (car form))))))))) (values expansion table)))) (defun standardize-form (form) (let ((prefix (ecase (length form) ;; no name (3 (first form)) (4 (second form)))) (params (ecase (length form) ;; no name (3 (second form)) (4 (third form)))) (outputs (ecase (length form) ;; no name (3 (third form)) (4 (fourth form))))) `(,(first form) ,(gentemp (symbol-name prefix)) ,params ,outputs))) (defparameter +block-param-keywords+ (list :params :outputs :locals)) (defun parse-block-params (param-block) "Extract the set of PARAMETER names, OUTPUT names and LOCAL variable names, and return them as three different values." (mapc #'(lambda (entry) (when (and (symbolp entry) (eq (symbol-package entry) (find-package :keyword)) (not (member entry +block-param-keywords+))) (error "Illegal keyword ~s in block parameter specification." entry))) param-block) (let (params outputs locals) (let* ((param-pos (position :params param-block)) (output-pos (position :outputs param-block)) (local-pos (position :locals param-block)) (all-pos (sort (remove nil (list param-pos output-pos local-pos)) #'<))) (flet ((next-pos (pos) (first (cdr (member pos all-pos))))) (when param-pos (setf params (subseq param-block (1+ param-pos) (next-pos param-pos)))) (when output-pos (let ((raw-outputs (subseq param-block (1+ output-pos) (next-pos output-pos)))) (setf outputs (iter (for output in raw-outputs) (cond ((symbolp output) (collecting `(,output ,output))) ((and (listp output) (= (length output) 2)) (collecting output)) (t (error "Unexpected output spec form: ~s" output))))))) (when local-pos (setf locals (subseq param-block (1+ local-pos) (next-pos local-pos)))) (values params outputs locals))))) (defun expand-block (form block-defs) (let* ((blockname (first form)) ;; used to standardize the local variable names (prefix (if (= (length form) 4) (concatenate 'string (symbol-name (second form)) "-") (concatenate 'string (symbol-name (gensym (symbol-name blockname))) "-"))) (param-bindings (if (= (length form) 4) (third form) (second form))) (output-bindings (if (= (length form) 4) (fourth form) (third form))) (blockdef (find blockname block-defs :key #'blockdef-name))) (or blockdef (error "No block named ~a is defined" blockname)) (let ((tmp (copy-tree (blockdef-body blockdef))) (outputs (copy-tree (blockdef-outputs blockdef))) table) ;; replace all the local names... (iter (for l in (blockdef-locals blockdef)) (as new-name = (intern (concatenate 'string prefix (symbol-name l)) :aiger-model)) (setf tmp (laig-subst new-name l tmp)) (setf outputs (mapcar #'(lambda (out) `(,(first out) ,(subst new-name l (second out)))) outputs))) ;; input names need to be substituted (iter (for i in (blockdef-params blockdef)) (as val = (second (find i param-bindings :key #'first))) (unless val (error "No binding for parameter ~a in invocation ~s" i form)) (setf tmp (laig-subst val i tmp)) (setf outputs (mapcar #'(lambda (out) `(,(first out) ,(subst val i (second out)))) outputs))) ;; outputs need to be recorded (iter (for (outname outval) in outputs) (as val = (second (find outname output-bindings :key #'first))) (unless val (error "No binding for output ~a in invocation ~s" outname form)) (when (eq val '_) (next-iteration)) ;ignore output (push (cons val outval) table)) (values tmp table)))) (defun laig-subst (new old laig-list) (mapcar #'(lambda (step) (laig-subst1 new old step)) laig-list)) (defun laig-subst1 (new old step) (case (first step) ((input and latch) (cons (first step) (subst new old (rest step)))) (t ;; proc invocation (destructuring-bind (procname locname params outputs) step `(,procname ,locname ,(iter (for (param-name val) in params) (collecting `(,param-name ,(subst new old val)))) ,(iter (for (param-name val) in outputs) (collecting `(,param-name ,(subst new old val))))))))) (defun translate-basic-model (model &key (stream t) symbol-table) (let ((name-table (make-hash-table :test 'eq)) inputs latches and-gates outputs) (when symbol-table (iter (for (name . literal) in symbol-table) (setf (gethash name name-table) literal))) (setf (gethash T name-table) 1 (gethash 'F name-table) 0) (assert (and (eq (first model) 'model) (symbolp (second model)) ; model name )) (flet ((translate-literal (lit) (translate-literal lit name-table)) (latch-name (latch) (first latch)) (latch-next (latch) (second latch)) (and-gate-name (and-gate) (first and-gate)) (and-gate-arg1 (and-gate) (second and-gate)) (and-gate-arg2 (and-gate) (third and-gate))) (iter (for form in (cddr model)) (case (car form) (input (num-args form 1) (push (second form) inputs)) (latch (num-args form 2) (push (rest form) latches)) (output (num-args form 1) (push (second form) outputs)) (and (num-args form 3) (push (rest form) and-gates)))) ;; emit the various model components in the order they ;; appear in the input (reverse the effects of accumulate by push). (setf inputs (nreverse inputs) outputs (nreverse outputs) latches (nreverse latches) and-gates (nreverse and-gates)) (let ((i 0)) (flet ((assign-indices (table) (iter (for var in table) (incf i) (setf (gethash var name-table) (* i 2))))) (assign-indices inputs) (assign-indices (mapcar #'latch-name latches)) (assign-indices (mapcar #'and-gate-name and-gates))) ;; i is now the index of the last variable (let ((numvars i)) (format stream "aag ~D ~D ~D ~D ~D~%" numvars (length inputs) (length latches) (length outputs) (length and-gates)))) (iter (for i from 2 to (* 2 (length inputs)) by 2) (format stream "~D~%" i)) (iter (for i from (* 2 (1+ (length inputs))) by 2) (as latch in latches) (format stream "~D ~D~%" i (translate-literal (latch-next latch)))) (iter (for x in outputs) (format stream "~D~%" (translate-literal x))) (iter (for i from (* 2 (+ 1 (length inputs) (length latches))) by 2) (as and-gate in and-gates) (format stream "~D ~D ~D~%" i (translate-literal (and-gate-arg1 and-gate)) (translate-literal (and-gate-arg2 and-gate)))) ;; symbol table (iter (for i from 2 by 2) (as input in inputs) (as j from 0) (format stream "i~d ~D~%" j i)) (iter (for i from (* 2 (1+ (length inputs))) by 2) (for j from 0) (as latch in latches) (format stream "l~d ~d~%" j i)) (iter (for i from 0) (as o in outputs) (format stream "o~d ~d~%" i (translate-literal o))) ;; comment (format stream "c~%") (format stream "model: ~a~%" (second model)) (iter (for input in inputs) (as j from 0) (format stream "i~d ~a ~D~%" j input (translate-literal input))) (iter (for latch in latches) (format stream "~a ~d next: ~a ~d~%" (latch-name latch) (translate-literal (latch-name latch)) (latch-next latch) (translate-literal (latch-next latch)))) (iter (for i from 0) (as o in outputs) (format stream "o~d ~s ~d~%" i o (translate-literal o)))))) (defun read-model-file (file) (let ((*package* (find-package :aiger-model))) (with-open-file (str file) (read str)))) QCHECK/aiger-model/examples/000755 000765 000024 00000000000 12332735360 016755 5ustar00fspedalistaff000000 000000 QCHECK/aiger-model/make-laigtoaig000755 000765 000024 00000000252 12332735323 017736 0ustar00fspedalistaff000000 000000 #! /bin/bash qcomp-buildapp --load ${HOME}/.sbclrc --eval '(qcomp)' --load-system "aiger-model" --entry 'aiger-model:translate-from-command-line' --output ~/bin/laigtoaigQCHECK/aiger-model/make-laigtoaig~000755 000765 000024 00000000255 12332735323 020137 0ustar00fspedalistaff000000 000000 #! /bin/bash qcomp-buildapp --load /Users/rpg/.sbclrc --eval '(qcomp)' --load-system "aiger-model" --entry 'aiger-model:translate-from-command-line' --output ~/bin/laigtoaigQCHECK/aiger-model/package.lisp000644 000765 000024 00000000207 12332735323 017421 0ustar00fspedalistaff000000 000000 ;;;; package.lisp (defpackage #:aiger-model (:use #:cl #:iterate) (:export #:translate-model #:translate-model-file)) QCHECK/aiger-model/README.txt000644 000765 000024 00000000100 12332735323 016623 0ustar00fspedalistaff000000 000000 A library to compose AIGER models using a simple lispy syntax. QCHECK/aiger-model/tests.lisp000644 000765 000024 00000003575 12332735323 017203 0ustar00fspedalistaff000000 000000 (in-package #:aiger-model) (defun compare-test (f1 f2) (compare-files (merge-pathnames (make-pathname :type "aag") f1) f2)) (defun compare-files (f1 f2) (asdf:run-shell-command "cmp ~a ~a" (namestring f1) (namestring f2))) (defun make-tempfile (template) (let ((tempdir (or (uiop:getenv "TEMPDIR") "/tmp"))) (with-input-from-string (x (uiop:run-program (format nil "mktemp ~a/~a" tempdir template) :output :string)) (read-line x)))) (defun translate-and-compare (laigfile) (let ((f2 (make-tempfile (format nil "~aXXX.aag" (pathname-name (parse-namestring (translate-logical-pathname laigfile))))))) (translate-model-file laigfile f2) (zerop (compare-test laigfile f2)))) (defun system-relative-namestring (sys name) (namestring (translate-logical-pathname (asdf:system-relative-pathname sys name)))) (fiveam:in-suite* aiger-model-tests) (fiveam:def-test simple-models () (fiveam:is-true (translate-and-compare (system-relative-namestring "aiger-model" "examples/and-gate.laig"))) (fiveam:is-true (translate-and-compare (system-relative-namestring "aiger-model" "examples/buffer.laig"))) (fiveam:is-true (translate-and-compare (system-relative-namestring "aiger-model" "examples/inverter.laig"))) (fiveam:is-true (translate-and-compare (system-relative-namestring "aiger-model" "examples/or-gate.laig"))) (fiveam:is-true (translate-and-compare (system-relative-namestring "aiger-model" "examples/toggle-flip-flop.laig"))) (fiveam:is-true (translate-and-compare (system-relative-namestring "aiger-model" "examples/toggle-with-enable-and-reset.laig")))) (fiveam:def-test nested-models () (fiveam:is-true (translate-and-compare (system-relative-namestring "aiger-model" "examples/adders.laig")))) QCHECK/aiger-model/examples/abstract-cegar.aag000644 000765 000024 00000005711 12332735360 022315 0ustar00fspedalistaff000000 000000 aag 127 9 40 1 78 2 4 6 8 10 12 14 16 18 20 2 22 4 24 6 26 8 28 10 30 12 32 15 34 14 36 6 38 6 40 2 42 2 44 6 46 12 48 17 50 16 52 57 54 131 56 129 58 36 60 38 62 40 64 42 66 44 68 46 70 36 72 38 74 40 76 42 78 44 80 46 82 249 84 251 86 18 88 82 90 84 92 88 94 90 96 92 98 94 254 100 32 109 102 34 113 104 101 103 106 37 39 108 106 41 110 47 45 112 110 43 114 48 123 116 50 127 118 115 117 120 37 39 122 120 41 124 47 45 126 124 43 128 57 55 130 118 118 132 58 60 134 132 62 136 58 60 138 136 64 140 58 60 142 140 66 144 58 62 146 144 64 148 58 62 150 148 66 152 58 64 154 152 66 156 60 62 158 156 64 160 60 62 162 160 66 164 60 64 166 164 66 168 62 64 170 168 66 172 135 139 174 143 147 176 151 155 178 159 163 180 167 171 182 172 174 184 176 178 186 180 182 188 184 186 190 70 72 192 190 74 194 70 72 196 194 76 198 70 72 200 198 78 202 70 74 204 202 76 206 70 74 208 206 78 210 70 76 212 210 78 214 72 74 216 214 76 218 72 74 220 218 78 222 72 76 224 222 78 226 74 76 228 226 78 230 193 197 232 201 205 234 209 213 236 217 221 238 225 229 240 230 232 242 234 236 244 238 240 246 242 244 248 87 246 250 86 246 252 96 98 254 252 52 i0 2 i1 4 i2 6 i3 8 i4 10 i5 12 i6 14 i7 16 i8 18 l0 20 l1 22 l2 24 l3 26 l4 28 l5 30 l6 32 l7 34 l8 36 l9 38 l10 40 l11 42 l12 44 l13 46 l14 48 l15 50 l16 52 l17 54 l18 56 l19 58 l20 60 l21 62 l22 64 l23 66 l24 68 l25 70 l26 72 l27 74 l28 76 l29 78 l30 80 l31 82 l32 84 l33 86 l34 88 l35 90 l36 92 l37 94 l38 96 l39 98 o0 254 c model: ABSTRACT i0 I0 2 i1 I1 4 i2 I2 6 i3 I3 8 i4 I4 10 i5 I5 12 i6 LEFT-INTEGRITY1-TOGGLE 14 i7 RIGHT-INTEGRITY6-TOGGLE 16 i8 TOGGLE-SWITCH 18 LI0 36 next: I0 2 LI1 38 next: I1 4 LI2 40 next: I2 6 LI3 42 next: I3 8 LI4 44 next: I4 10 LI5 46 next: I5 12 LEFT-INTEGRITY1-CONSTRAINT1 32 next: (NOT LEFT-INTEGRITY1-TOGGLE) 15 LEFT-INTEGRITY1-CONSTRAINT2 34 next: LEFT-INTEGRITY1-TOGGLE 14 LI0 36 next: I2 6 LI1 38 next: I2 6 LI2 40 next: I0 2 LI3 42 next: I0 2 LI4 44 next: I2 6 LI5 46 next: I5 12 RIGHT-INTEGRITY6-CONSTRAINT1 48 next: (NOT RIGHT-INTEGRITY6-TOGGLE) 17 RIGHT-INTEGRITY6-CONSTRAINT2 50 next: RIGHT-INTEGRITY6-TOGGLE 16 VALID 52 next: (NOT INVALID) 57 TRACE-VALID11-L1 54 next: CONSTRAINTS-NOT-ENFORCED 131 TRACE-VALID11-ONE-SHOT 56 next: ONE-SHOT-VAL 129 THREE-OF-ENABLEMENT14-LLI0 58 next: LI0 36 THREE-OF-ENABLEMENT14-LLI1 60 next: LI1 38 THREE-OF-ENABLEMENT14-LLI2 62 next: LI2 40 THREE-OF-ENABLEMENT14-LLI3 64 next: LI3 42 THREE-OF-ENABLEMENT14-LLI4 66 next: LI4 44 THREE-OF-ENABLEMENT14-LLI5 68 next: LI5 46 THREE-OF-ENABLEMENT34-LLI0 70 next: RLI0 36 THREE-OF-ENABLEMENT34-LLI1 72 next: RLI1 38 THREE-OF-ENABLEMENT34-LLI2 74 next: RLI2 40 THREE-OF-ENABLEMENT34-LLI3 76 next: RLI3 42 THREE-OF-ENABLEMENT34-LLI4 78 next: RLI4 44 THREE-OF-ENABLEMENT34-LLI5 80 next: RLI5 46 LEFT 82 next: LEFT-ON 249 RIGHT 84 next: RIGHT-ON 251 LR-SWITCH 86 next: TOGGLE-SWITCH 18 LEFT1 88 next: LEFT 82 RIGHT1 90 next: RIGHT 84 LEFT2 92 next: LEFT1 88 RIGHT2 94 next: RIGHT1 90 LEFT3 96 next: LEFT2 92 RIGHT3 98 next: RIGHT2 94 o0 AIGER-MODEL::OUTVAL 254 QCHECK/aiger-model/examples/abstract-cegar.aig000644 000765 000024 00000004071 12332735360 022323 0ustar00fspedalistaff000000 000000 aig 91 9 40 1 42 2 4 6 8 10 12 15 14 6 6 2 2 6 12 17 16 57 115 117 36 38 40 42 44 46 36 38 40 42 44 46 177 179 18 82 84 88 90 92 94 182 =;7;?;;,(.,64:6 @>DBNLRNXRZX "WXR€i0 2 i1 4 i2 6 i3 8 i4 10 i5 12 i6 14 i7 16 i8 18 l0 20 l1 22 l2 24 l3 26 l4 28 l5 30 l6 32 l7 34 l8 36 l9 38 l10 40 l11 42 l12 44 l13 46 l14 48 l15 50 l16 52 l17 54 l18 56 l19 58 l20 60 l21 62 l22 64 l23 66 l24 68 l25 70 l26 72 l27 74 l28 76 l29 78 l30 80 l31 82 l32 84 l33 86 l34 88 l35 90 l36 92 l37 94 l38 96 l39 98 o0 254 c model: ABSTRACT i0 I0 2 i1 I1 4 i2 I2 6 i3 I3 8 i4 I4 10 i5 I5 12 i6 LEFT-INTEGRITY1-TOGGLE 14 i7 RIGHT-INTEGRITY6-TOGGLE 16 i8 TOGGLE-SWITCH 18 LI0 36 next: I0 2 LI1 38 next: I1 4 LI2 40 next: I2 6 LI3 42 next: I3 8 LI4 44 next: I4 10 LI5 46 next: I5 12 LEFT-INTEGRITY1-CONSTRAINT1 32 next: (NOT LEFT-INTEGRITY1-TOGGLE) 15 LEFT-INTEGRITY1-CONSTRAINT2 34 next: LEFT-INTEGRITY1-TOGGLE 14 LI0 36 next: I2 6 LI1 38 next: I2 6 LI2 40 next: I0 2 LI3 42 next: I0 2 LI4 44 next: I2 6 LI5 46 next: I5 12 RIGHT-INTEGRITY6-CONSTRAINT1 48 next: (NOT RIGHT-INTEGRITY6-TOGGLE) 17 RIGHT-INTEGRITY6-CONSTRAINT2 50 next: RIGHT-INTEGRITY6-TOGGLE 16 VALID 52 next: (NOT INVALID) 57 TRACE-VALID11-L1 54 next: CONSTRAINTS-NOT-ENFORCED 131 TRACE-VALID11-ONE-SHOT 56 next: ONE-SHOT-VAL 129 THREE-OF-ENABLEMENT14-LLI0 58 next: LI0 36 THREE-OF-ENABLEMENT14-LLI1 60 next: LI1 38 THREE-OF-ENABLEMENT14-LLI2 62 next: LI2 40 THREE-OF-ENABLEMENT14-LLI3 64 next: LI3 42 THREE-OF-ENABLEMENT14-LLI4 66 next: LI4 44 THREE-OF-ENABLEMENT14-LLI5 68 next: LI5 46 THREE-OF-ENABLEMENT34-LLI0 70 next: RLI0 36 THREE-OF-ENABLEMENT34-LLI1 72 next: RLI1 38 THREE-OF-ENABLEMENT34-LLI2 74 next: RLI2 40 THREE-OF-ENABLEMENT34-LLI3 76 next: RLI3 42 THREE-OF-ENABLEMENT34-LLI4 78 next: RLI4 44 THREE-OF-ENABLEMENT34-LLI5 80 next: RLI5 46 LEFT 82 next: LEFT-ON 249 RIGHT 84 next: RIGHT-ON 251 LR-SWITCH 86 next: TOGGLE-SWITCH 18 LEFT1 88 next: LEFT 82 RIGHT1 90 next: RIGHT 84 LEFT2 92 next: LEFT1 88 RIGHT2 94 next: RIGHT1 90 LEFT3 96 next: LEFT2 92 RIGHT3 98 next: RIGHT2 94 o0 AIGER-MODEL::OUTVAL 254 QCHECK/aiger-model/examples/abstract-cegar.laig000644 000765 000024 00000044210 12332735360 022476 0ustar00fspedalistaff000000 000000 (model abstract (defblock alias (:params to :outputs (from to))) (defblock and3 (:params x y z :locals and1 and2 :outputs (val and2)) (and and1 x y) (and and2 and1 z)) (defblock and4 (:params w x y z :locals and1 and2 and3 :outputs (val and3)) (and and1 w x) (and and2 y z) (and and3 and1 and2)) (defblock or-gate (:params x y :locals gate :outputs (val (not gate))) (and gate (not x) (not y))) ;; the return value of this function will turn on forever if the input ;; ever rises to 1 from zero. (defblock only-once (:params input :outputs (val one-shot) :locals one-shot tmp l1) (latch l1 input) ; will rise and fall (latch one-shot one-shot-val) (or-gate tmp ((x one-shot) (y l1)) ((val one-shot-val)))) ;; This abstract model attempts to find a very simple CEGAR problem. (input i0) (input i1) (input i2) (input i3) (input i4) (input i5) ;; block that captures integrity checking on the system inputs. (defblock integrity (:params i0 i1 i2 i3 i4 i5 :locals toggle constraint1 constraint2 constraint1-val constraint2-val c1-enforcedp c2-enforcedp :outputs li0 li1 li2 li3 li4 li5 constraints-enforced ) ;; first we latch the inputs (latch li0 i0) (latch li1 i1) (latch li2 i2) (latch li3 i3) (latch li4 i4) (latch li5 i5) ;; depending on the input, we decide which constraint to enforce (input toggle) (latch constraint1 (not toggle)) (latch constraint2 toggle) (or-gate ce1 ((x (not constraint1)) (y constraint1-val)) ((val c1-enforcedp))) (or-gate ce2 ((x (not constraint2)) (y constraint2-val)) ((val c2-enforcedp))) (and constraints-enforced c1-enforcedp c2-enforcedp) (and3 constraint1 ((x (not li0)) (y (not li1)) (z (not li2))) ((val constraint1-val))) (and3 constraint2 ((x (not li5)) (y (not li4)) (z (not li3))) ((val constraint2-val))) ) (integrity left-integrity ((i0 i0) (i1 i1) (i2 i2) (i3 i3) (i4 i4) (i5 i5)) ((li0 li0) (li1 li1) (li2 li2) (li3 li3) (li4 li4) (li5 li5) (constraints-enforced left-constraints-enforced))) (integrity right-integrity ((i0 i1) (i1 i4) (i2 i3) (i3 i0) (i4 i2) (i5 i5)) ((li0 rli0) (li1 rli1) (li2 rli2) (li3 rli3) (li4 rli4) (li5 rli5) (constraints-enforced right-constraints-enforced))) ;; (alias ((to (not toggle))) ((from constraint1))) ;; (alias ((to toggle)) ((from constraint2))) (latch valid (not invalid)) (only-once trace-valid ((input constraints-not-enforced)) ((val invalid))) (or-gate constraints-not-enforced ((x (not left-constraints-enforced)) (y (not right-constraints-enforced))) ((val constraints-not-enforced))) (defblock three-of-enablement (:params li0 li1 li2 li3 li4 li5 :locals and-out0 and-out1 and-out2 and-out3 and-out4 and-out5 and-out6 and-out7 and-out8 and-out9 disj0 disj1 disj2 disj3 disj4 disj5 disj6 disj7 lli0 lli1 lli2 lli3 lli4 lli5 :outputs (val one-triple)) ;; one cycle delay for processing (latch lli0 li0) (latch lli1 li1) (latch lli2 li2) (latch lli3 li3) (latch lli4 li4) (latch lli5 li5) ;; this large block is to choose three of the inputs (and3 c0 ((x lli0) (y lli1) (z lli2)) ((val and-out0))) (and3 c1 ((x lli0) (y lli1) (z lli3)) ((val and-out1))) (and3 c2 ((x lli0) (y lli1) (z lli4)) ((val and-out2))) (and3 c3 ((x lli0) (y lli2) (z lli3)) ((val and-out3))) (and3 c4 ((x lli0) (y lli2) (z lli4)) ((val and-out4))) (and3 c5 ((x lli0) (y lli3) (z lli4)) ((val and-out5))) (and3 c6 ((x lli1) (y lli2) (z lli3)) ((val and-out6))) (and3 c7 ((x lli1) (y lli2) (z lli4)) ((val and-out7))) (and3 c8 ((x lli1) (y lli3) (z lli4)) ((val and-out8))) (and3 c9 ((x lli2) (y lli3) (z lli4)) ((val and-out9))) (or-gate co0 ((x and-out0) (y and-out1)) ((val disj0))) (or-gate co1 ((x and-out2) (y and-out3)) ((val disj1))) (or-gate co2 ((x and-out4) (y and-out5)) ((val disj2))) (or-gate co3 ((x and-out6) (y and-out7)) ((val disj3))) (or-gate co4 ((x and-out8) (y and-out9)) ((val disj4))) (or-gate co5 ((x disj0) (y disj1)) ((val disj5))) (or-gate co6 ((x disj2) (y disj3)) ((val disj6))) (or-gate co7 ((x disj4) (y disj5)) ((val disj7))) (or-gate co8 ((x disj6) (y disj7)) ((val one-triple)))) (three-of-enablement ((li0 li0) (li1 li1) (li2 li2) (li3 li3) (li4 li4) (li5 li5)) ((val left-triple))) (three-of-enablement ((li0 rli0) (li1 rli1) (li2 rli2) (li3 rli3) (li4 rli4) (li5 rli5)) ((val right-triple))) ;; (and4 ca0 ((w lli0) (x lli1) (y lli2) (z lli3)) ((val ca-out0))) ;; (and4 ca1 ((w lli0) (x lli1) (y lli2) (z lli4)) ((val ca-out1))) ;; (and4 ca2 ((w lli0) (x lli1) (y lli3) (z lli4)) ((val ca-out2))) ;; (and4 ca3 ((w lli0) (x lli2) (y lli3) (z lli4)) ((val ca-out3))) ;; (and4 ca4 ((w lli1) (x lli2) (y lli3) (z lli4)) ((val ca-out4))) ;; (or-gate co0 ((x ca-out0) (y ca-out1)) ((val disj1-0))) ;; (or-gate co1 ((x ca-out2) (y ca-out3)) ((val disj1-1))) ;; (or-gate co2 ((x ca-out4) (y disj1-0)) ((val disj1-2))) ;; (or-gate co3 ((x disj1-2) (y disj1-2)) ((val one-quad))) (latch left left-on) (latch right right-on) (or-gate left-on ((x lr-switch) (y left-triple)) ((val left-on))) (or-gate right-on ((x (not lr-switch)) (y right-triple)) ((val right-on))) (input toggle-switch) (latch lr-switch toggle-switch) ;;(and checked-right right-on (not one-quad)) ;; get another delay cycle to let the validity check catch up. (latch left1 left) (latch right1 right) (latch left2 left1) (latch right2 right1) (latch left3 left2) (latch right3 right2) (and both left3 right3) ;; the circuit is unsafe if both sides are on in a valid trace. (and outval both valid) (output outval) ;; (latch q1 one-quad) ;; (latch q2 q1) ;; (and check-val valid q2) ;; (output check-val) ;; (defblock alias (:params to :outputs (from to))) ;; (defblock xor-gate (:params x y ;; :locals conj and-not gate ;; :outputs (val gate)) ;; (and conj x y) ;; (and and-not (not x) (not y)) ;; (and gate (not and-not) (not conj))) ;; ;; (defblock no-others (:params o1 o2 o3 ;; ;; :locals tmp1 tmp2 ;; ;; :outputs (val tmp1)) ;; ;; (and tmp1 (not o1) tmp2) ;; ;; (and tmp2 (not o2) (not o3))) ;; ;; (defblock persist (:params now o1 o2 o3 ;; ;; :locals persist no-others ;; ;; :outputs (persist persist)) ;; ;; (no-others persist-no-others ((o1 o1) (o2 o2) (o3 o3)) ((val no-others))) ;; ;; (and persist now no-others)) ;; ;; (defblock rising-edge (:params now last ;; ;; :locals rising ;; ;; :outputs (val rising)) ;; ;; (and rising now (not last))) ;; (defblock only-once (:params input ;; :outputs (val one-shot) ;; :locals one-shot tmp l1) ;; (latch l1 input) ; will rise and fall ;; (latch one-shot one-shot-val) ;; (or-gate tmp ((x one-shot) (y l1)) ((val one-shot-val)))) ;; ;; (only-once powering-up ((input power-up-in)) ((val power))) ;; ;; (latch chg-coupled-side chg-coupled-side-in) ;; ;; (latch hdg-switch hdg-switch-in) ;; ;; (latch hdg-switch-not-vappr no-vappr-check) ;; ;; (latch sync-switch sync-switch-in) ;; ;; (latch ga-switch ga-switch-in) ;; ;; (alias ((to go-around-on)) ((from vga))) ;; ;; (or-gate vga-manual-or-auto ((x vga-switch-in)(y (not vappr))) ((val go-around-on))) ;; ;; ;; (latch vga vga-switch-in) ;; ;; (latch not-vga (not vga-switch-in)) ;; ;; (latch lappr-capture lappr-captured) ;; ;; ;; change so that lapp-captured only when ;; ;; ;; Vertical Approach is already captured. ;; ;; (and lappr-captured lappr-capture-in vappr) ;; ;; (and no-vappr-check hdg-switch-in (not vappr)) ;; ;; (input power-up-in) ;; ;; (input chg-coupled-side-in) ;; ;; (input hdg-switch-in) ;; ;; (input sync-switch-in) ;; ;; (input ga-switch-in) ;; ;; (input vga-switch-in) ;; ;; (input lappr-capture-in) ;; ;; ;; add logic to check for VAPPR... ;; ;; ;; this is a little bit made up.... ;; ;; ;;(latch vappr vappr-check) ;; ;; (alias ((to vappr-check)) ((from vappr))) ;; ;; (input vappr1) ;; ;; (input vappr2) ;; ;; (input vappr3) ;; ;; (input vappr4) ;; ;; (input vappr5) ;; ;; (input vappr6) ;; ;; ;; vappr inputs must be positive for three counts... ;; ;; (latch v11 vappr1) ;; ;; (latch v12 vappr2) ;; ;; (latch v13 vappr3) ;; ;; (latch v21 v11) ;; ;; (latch v22 v12) ;; ;; (latch v23 v13) ;; ;; (latch v31 vappr4) ;; ;; (latch v32 vappr5) ;; ;; (latch v33 vappr6) ;; ;; (and vappr-check v11 vc2) ;; ;; (and vc2 v12 vc3) ;; ;; (and vc3 v13 vc4) ;; ;; (and vc4 v21 vc5) ;; ;; (and vc5 v22 vc6) ;; ;; (and vc6 v23 vc7) ;; ;; (and vc7 v31 vc8) ;; ;; (and vc8 v32 v33) ;; ;; (latch last-power power) ;; ;; (latch last-chg-coupled-side chg-coupled-side) ;; ;; (latch last-hdg-switch hdg-switch) ;; ;; (latch last-hdg-switch-not-vappr hdg-switch-not-vappr) ;; ;; (latch last-sync-switch sync-switch) ;; ;; (latch last-ga-switch ga-switch) ;; ;; (latch last-vga vga) ;; ;; (latch last-not-vga not-vga) ;; ;; (latch last-lappr-capture lappr-capture) ;; ;; (latch roll roll-enable) ;; ;; (latch hdg hdg-enable) ;; ;; (latch lappr lappr-enable) ;; ;; (latch lga lga-enable) ;; ;; ;; rising edges ;; ;; (rising-edge power-up ((now power) (last last-power)) ((val power-up-rising))) ;; ;; (rising-edge chg-coupled-side ((now chg-coupled-side) (last last-chg-coupled-side)) ;; ;; ((val chg-coupled-side-rising))) ;; ;; (rising-edge hdg-switch ((now hdg-switch) (last last-hdg-switch)) ((val hdg-switch-rising))) ;; ;; (rising-edge hdg-switch-not-vappr ((now hdg-switch-not-vappr) (last last-hdg-switch-not-vappr)) ;; ;; ((val hdg-switch-not-vappr-rising))) ;; ;; (rising-edge sync-switch ((now sync-switch) (last last-sync-switch)) ((val sync-switch-rising))) ;; ;; (rising-edge ga-switch ((now ga-switch) (last last-ga-switch)) ((val ga-switch-rising))) ;; ;; (rising-edge vga ((now vga) (last last-vga)) ((val vga-rising))) ;; ;; (rising-edge not-vga ((now not-vga) (last last-not-vga)) ((val not-vga-rising))) ;; ;; (rising-edge lappr-capture ((now lappr-capture) (last last-lappr-capture)) ((val lappr-capture-rising))) ;; ;; ;; roll enable logic ;; ;; (or-gate roll-enable ((x roll-persist) (y roll-enable-on)) ((val roll-enable))) ;; ;; (persist roll-persist ((now roll) (o1 hdg-enable-on) (o2 lappr-enable-on) (o3 lga-enable-on)) ((persist roll-persist))) ;; ;; (or-gate ((x reo1) (y power-up-rising)) ((val roll-enable-on))) ;; ;; (and reo1 chg-coupled-side-rising reo2) ;; ;; (and reo2 hdg-switch-rising reo3) ;; ;; (and reo3 sync-switch-rising reo4) ;; ;; (and reo4 (not roll) not-vga-rising) ;; ;; ;; hdg enable logic ;; ;; (or-gate hdg-enable ((x hdg-persist) (y hdg-enable-on)) ((val hdg-enable))) ;; ;; (persist hdg-persist ((now hdg) (o1 roll-enable-on) (o2 lappr-enable-on) (o3 lga-enable-on)) ((persist hdg-persist))) ;; ;; (and hdg-enable-on (not power-up-rising) heo1) ;; ;; (and heo1 hdg-switch-rising heo2) ;; ;; (and heo2 hdg-switch-not-vappr-rising heo3) ;; ;; (and heo3 power heo4) ;; ;; (and heo4 (not hdg) (not roll-enable-on)) ; ROLL takes precedence over HDG. ;; ;; ;; lappr-enable logic ;; ;; (or-gate lappr-enable ((x lappr-persist) (y lappr-enable-on)) ((val lappr-enable))) ;; ;; (persist lappr-persist ((now lappr) (o1 vappr) (o2 hdg-enable-on) (o3 lga-enable-on)) ((persist lappr-persist))) ;; ;; (and lappr-enable-on (not power-up-rising) laeo1) ;; ;; (and laeo1 (not lappr) laeo2) ;; ;; (and laeo2 power laeo3) ;; ;; (and laeo3 lappr-capture-rising laeo4) ;; ;; ;; the next two capture heading taking precedence over LAPPR. ;; ;; (and laeo4 (not sync-switch-rising) laeo5) ;; ;; (and laeo5 (not hdg-switch-rising) laeo6) ;; ;; (and laeo6 vappr (not ga-switch-rising)) ; go-around breaks out of lateral approach ;; ;; ;; lga-enable logic ;; ;; (or-gate lga-enable ((x lga-persist) (y lga-enable-on)) ((val lga-enable))) ;; ;; (persist lga-persist ((now lga) (o1 roll-enable-on) (o2 hdg-enable-on) (o3 lappr-enable-on)) ((persist lga-persist))) ;; ;; (and lga-enable-on (not power-up-rising) leo1) ;; ;; (and leo1 ga-switch-rising leo2) ;; ;; (and leo2 vga-rising leo3) ;; ;; (and leo3 (not lga) leo4) ;; ;; (and leo4 power (not hdg-enable-on)) ; HDG wins over LGA according to the paper. ;; ;; ;; FIXME: LAPPR should be required to be the previous state... ;; ;; (or-gate top-o ((x pair1) (y bad1)) ((val bad))) ;; ;; (and pair1 roll hdg) ;; ;; (or-gate ((x pair2) (y bad2)) ((val bad1))) ;; ;; (and pair2 roll lappr) ;; ;; (or-gate ((x pair3) (y bad3)) ((val bad2))) ;; ;; (and pair3 roll lga) ;; ;; (or-gate ((x pair4) (y bad4)) ((val bad3))) ;; ;; (and pair4 hdg lappr) ;; ;; (or-gate ((x pair5) (y pair6)) ((val bad4))) ;; ;; (and pair5 hdg lga) ;; ;; (and pair6 lappr lga) ;; ;; ground approach transmission. this is the true state ;; (input GA) ;; ;; when its on, ;; (only-once ga-state ((input GA)) ((val true-ga-val))) ;; (input ga-error) ;; (only-once ga-sense1 ((input ga-sense1)) ((val ga-sense1-latch))) ;; (only-once ga-sense2 ((input ga-sense2)) ((val ga-sense2-latch))) ;; (only-once ga-sense3 ((input ga-sense3)) ((val ga-sense3-latch))) ;; ;; need to latch three values... ;; (and ga-sense1 true-ga-val (not ga-error)) ;; (and ga-sense2 ga-sense1-latch ga-good) ;; (and ga-good true-ga-val (not ga-error)) ;; (and ga-sense3 ga-sense2-latch ga-good) ;; (only-once ga-error1 ((input ga-error)) ((val one-ga-error))) ;; (only-once ga-error2 ((input ga-error2)) ((val two-ga-errors))) ;; (and ga-error2 one-ga-error ga-error) ;; (input input1) ;; (input input2) ;; (input input3) ;; (input input4) ;; (latch common1 input1) ;; (latch common2 input2) ;; (latch common3 input3) ;; (latch common4 input4) ;; (input ground-approach-switch) ;; (input ground-approach-disable-switch) ;; (only-once ground-approach-disablement ;; ((input ground-approach-disable-switch)) ((val ground-approach-disabled))) ;; (input ground-approach-failure) ;; (only-once ground-approach-disablement2 ;; ((input ground-approach-failure)) ((val ground-approach-failed))) ;; (xor-gate ground-approach-unavailable ((x ground-approach-disabled) (y ground-approach-failed)) ;; ((val ground-approach-unavailable))) ;; ;; we begin ground approach one tick after we have securely sensed it ;; ;; and the pilot engages the switch ;; (and engage-ground-approach ground-approach-switch-on ga-sense3-latch) ;; (and ground-approach-switch-on ground-approach-switch (not ground-approach-unavailable)) ;; ;;; FINAL stage in current search, we jump to turning both on, because the ;; ;;; true GA state is an input at 0 and so is ground-approach-disabled. ;; ;;; can we find multiple values for these? ;; ;; auto-pilot ;; (input autopilot-switch) ;; (only-once auto-pilot-engagement ((input autopilot-switch)) ((val autopilot-switch-on))) ;; ;; ;; (and autopilot-on autopilot-switch-on (not true-GA-val)) ;; (latch mode1-specific engage-ground-approach) ;; (latch mode2-specific autopilot-on) ;; (and ground-approach-on all-common mode1-specific) ;; (and level-flight-on all-common mode2-specific) ;; (and all-common ac1 ac2) ;; (and ac1 common1 common2) ;; (and ac2 common3 common4) ;; (latch ground-approach ground-approach-on) ;; (latch level-flight level-flight-on) ;; ;; this captures conditions that we consider cannot happen in our model. ;; (latch valid (not ga-error2)) ;; (and bad ground-approach level-flight) ;; ;; we reject model failures ;; (and valid-bad bad valid) ;; ;; violation of safety property. ;; (output valid-bad)) ) QCHECK/aiger-model/examples/adders.aag000644 000765 000024 00000000161 12332735360 020667 0ustar00fspedalistaff000000 000000 aag 6 2 0 1 4 2 4 12 6 2 4 8 3 5 10 7 9 12 2 4 i0 2 i1 4 o0 12 c model: ADDERS i0 XIN 2 i1 YIN 4 o0 CARRY-OUT 12 QCHECK/aiger-model/examples/adders.laig000644 000765 000024 00000001125 12332735360 021054 0ustar00fspedalistaff000000 000000 (model adders (defblock xor-gate (:params x y :outputs (val xor) :locals conj neither xor) (and conj x y) (and neither (not x) (not y)) (and xor (not conj) (not neither))) (defblock half-adder (:params x y :outputs (carry and) (sum xor) :locals xor and) (xor-gate xor ((x x) (y y)) ((val xor))) (and and x y)) (input xin) (input yin) (output carry-out) (half-adder add1 ((x xin) (y yin)) ((carry carry-out) (sum _)))) QCHECK/aiger-model/examples/and-gate.aag000644 000765 000024 00000000122 12332735360 021102 0ustar00fspedalistaff000000 000000 aag 3 2 0 1 1 2 4 6 6 2 4 i0 2 i1 4 o0 6 c model: AND-GATE i0 I0 2 i1 I1 4 o0 O 6 QCHECK/aiger-model/examples/and-gate.laig000644 000765 000024 00000000110 12332735360 021263 0ustar00fspedalistaff000000 000000 (model and-gate (input i0) (input i1) (and o i0 i1) (output o)) QCHECK/aiger-model/examples/buffer-nosym.aig000644 000765 000024 00000000020 12332735360 022043 0ustar00fspedalistaff000000 000000 aig 1 1 0 1 0 2 QCHECK/aiger-model/examples/buffer.aag000644 000765 000024 00000000074 12332735360 020701 0ustar00fspedalistaff000000 000000 aag 1 1 0 1 0 2 2 i0 2 o0 2 c model: BUFFER i0 I0 2 o0 I0 2 QCHECK/aiger-model/examples/buffer.laig000644 000765 000024 00000000052 12332735360 021061 0ustar00fspedalistaff000000 000000 (model buffer (input i0) (output i0)) QCHECK/aiger-model/examples/bus-example.laig000644 000765 000024 00000007531 12332735360 022043 0ustar00fspedalistaff000000 000000 (model bus-example ;; four line encoder (latch sem0 nextsem0) (latch sem1 nextsem1) (latch sem2 nextsem2) (latch sem3 nextsem3) (defblock or-gate (:params x y :locals gate :outputs (val (not gate))) (and gate (not x) (not y))) (defblock semaphore (:params p0 p1 p2 p3 ; requests v0 v1 v2 v3 ; drops s0 s1 s2 s3 ; current values :locals none none1 none2 :outputs (l0 l0) (l1 l1) (l2 l2) (l3 l3)) (sem-party sem-party0 ((mysem s0) (myreq p0) (mydrop v0) (none none) (or1 p1) (or2 p2) (or3 p3)) ((newsem l0))) (sem-party sem-party1 ((mysem s1) (myreq p1) (mydrop v1) (none none) (or1 p0) (or2 p2) (or3 p3)) ((newsem l1))) (sem-party sem-party2 ((mysem s2) (myreq p2) (mydrop v2) (none none) (or1 p0) (or2 p1) (or3 p3)) ((newsem l2))) (sem-party sem-party3 ((mysem s3) (myreq p3) (mydrop v3) (none none) (or1 p1) (or2 p2) (or3 p0)) ((newsem l3))) ;; (or-gate zero keep-zero get-zero) ;; (and keep-zero s0 (not v0)) ;; (and get-zero none req0) ;; (and req0 p0 no-others0) ;; (and no-others01 (not p1) (not p2)) ;; (and no-others0 no-others01 (not p3)) (and none none1 none2) (and none1 (not s0) (not s1)) (and none2 (not s2) (not s3))) (defblock sem-party (:params mysem myreq mydrop or1 or2 or3 ; other requests none :locals my-get my-keep my-val reqtmp no-others no-others1 :outputs (newsem my-val)) ;; ln = (ln & -vn) | (\sum -l0..-ln & pn & \prod -pi, i \neq n) (or-gate or-gate1 ((x my-get) (y my-keep)) ((val my-val))) (and my-keep mysem (not mydrop)) (and my-get none reqtmp) (and reqtmp myreq no-others) (and no-others (not or1) no-others1) (and no-others1 (not or2) (not or3))) (defblock bus-writer (:params mysem :locals do-write do-drop :outputs (p do-write) (v do-drop)) (input write) (input stop-writing) (and do-write (not mysem) write) (and do-drop mysem stop-writing)) (semaphore sem ((p0 p0) (p1 p1) (p2 p2) (p3 p3) (p4 p4) (v0 v0) (v1 v1) (v2 v2) (v3 v3) (v4 v4) (s0 sem0) (s1 sem1) (s2 sem2) (s3 sem3)) ((l0 nextsem0) (l1 nextsem1) (l2 nextsem2) (l3 nextsem3))) (bus-writer wr0 ((mysem sem0)) ((p p0)(v v0))) (bus-writer wr1 ((mysem sem1)) ((p p1)(v v1))) (bus-writer wr2 ((mysem sem2)) ((p p2)(v v2))) (bus-writer wr3 ((mysem sem3)) ((p p3)(v v3))) (or-gate top-o ((x pair1) (y bad1)) ((val bad))) (and pair1 sem0 sem1) (or-gate ((x pair2) (y bad2)) ((val bad1))) (and pair2 sem0 sem2) (or-gate ((x pair3) (y bad3)) ((val bad2))) (and pair3 sem0 sem3) (or-gate ((x pair4) (y bad4)) ((val bad3))) (and pair4 sem1 sem2) (or-gate ((x pair5) (y pair6)) ((val bad4))) (and pair5 sem1 sem3) (and pair6 sem2 sem3) ;; violation of safety property. (output bad)) QCHECK/aiger-model/examples/cegar-test1.aag000644 000765 000024 00000000265 12332735360 021551 0ustar00fspedalistaff000000 000000 aag 5 0 3 1 2 2 3 4 5 6 7 11 8 3 5 10 8 7 l0 2 l1 4 l2 6 o0 11 c model: CEGAR-TEST1 DISJ1 2 next: (NOT DISJ1) 3 DISJ2 4 next: (NOT DISJ2) 5 DISJ3 6 next: (NOT DISJ3) 7 o0 TOP-OR 11 QCHECK/aiger-model/examples/cegar-test1.laig000644 000765 000024 00000000765 12332735360 021742 0ustar00fspedalistaff000000 000000 (model cegar-test1 (latch disj1 (not disj1)) (latch disj2 (not disj2)) (latch disj3 (not disj3)) (or-gate ((d1 disj1) (d2 disj2)) ((val or1))) (or-gate ((d1 or1) (d2 disj3)) ((val top-or))) (output top-or) (defblock or-gate (:params d1 d2 :outputs (val (not tmp)) :locals tmp) (and tmp (not d1) (not d2))) ) QCHECK/aiger-model/examples/cegar-test2.aag000644 000765 000024 00000001321 12332735360 021544 0ustar00fspedalistaff000000 000000 aag 32 3 9 1 20 2 4 6 8 36 10 48 12 60 14 34 16 40 18 46 20 52 22 58 24 64 29 26 9 11 28 26 13 30 14 2 32 15 3 34 33 31 36 16 30 38 17 31 40 39 37 42 18 4 44 19 5 46 45 43 48 20 42 50 21 43 52 51 49 54 22 6 56 23 7 58 57 55 60 24 54 62 25 55 64 63 61 i0 2 i1 4 i2 6 l0 8 l1 10 l2 12 l3 14 l4 16 l5 18 l6 20 l7 22 l8 24 o0 29 c model: CEGAR-TEST2 i0 COUNTER0-CIN 2 i1 COUNTER1-CIN 4 i2 COUNTER2-CIN 6 DISJ1 8 next: NEXTL0 36 DISJ2 10 next: NEXTL1 48 DISJ3 12 next: NEXTL2 60 COUNTER0-L0 14 next: COUNTER0-NEXT0 34 COUNTER0-L1 16 next: COUNTER0-NEXT1 40 COUNTER1-L0 18 next: COUNTER1-NEXT0 46 COUNTER1-L1 20 next: COUNTER1-NEXT1 52 COUNTER2-L0 22 next: COUNTER2-NEXT0 58 COUNTER2-L1 24 next: COUNTER2-NEXT1 64 o0 TOP-OR 29 QCHECK/aiger-model/examples/cegar-test2.laig000644 000765 000024 00000002260 12332735360 021733 0ustar00fspedalistaff000000 000000 (model cegar-test2 (latch disj1 nextl0) (latch disj2 nextl1) (latch disj3 nextl2) (or-gate ((d1 disj1) (d2 disj2)) ((val or1))) (or-gate ((d1 or1) (d2 disj3)) ((val top-or))) (output top-or) (defblock or-gate (:params d1 d2 :outputs (val (not tmp)) :locals tmp) (and tmp (not d1) (not d2))) (defblock counter (:params :outputs (val carry-out) :locals cin l0 l1 c0 none0 next0 carry-out none1 next1 ) (input cin) (latch l0 next0) (and c0 l0 cin) ; carry out of first bit (and none0 (not l0) (not cin)) (and next0 (not none0) (not c0)) ; cin ^ l0 (latch l1 next1) (and carry-out l1 c0) (and none1 (not l1) (not c0)) (and next1 (not none1) (not carry-out))) (counter counter0 () ((val nextl0))) (counter counter1 () ((val nextl1))) (counter counter2 () ((val nextl2))) ) QCHECK/aiger-model/examples/cegar-test3.aag000644 000765 000024 00000003301 12332735360 021545 0ustar00fspedalistaff000000 000000 aag 75 12 21 1 42 2 4 6 8 10 12 14 16 18 20 22 24 26 103 28 88 30 74 32 134 34 3 36 4 38 122 40 6 42 8 44 10 46 12 48 14 50 16 52 108 54 114 56 120 58 126 60 132 62 138 64 144 66 150 71 68 27 29 70 68 31 72 32 40 74 72 85 76 36 42 78 36 44 80 42 44 82 77 79 84 82 81 86 38 46 88 86 99 90 101 48 92 101 50 94 48 50 96 91 93 98 96 95 100 33 147 102 111 35 104 52 18 106 53 19 108 107 105 110 54 104 112 55 105 114 113 111 116 56 20 118 57 21 120 119 117 122 58 116 124 59 117 126 125 123 128 60 22 130 61 23 132 131 129 134 62 128 136 63 129 138 137 135 140 64 24 142 65 25 144 143 141 146 66 140 148 67 141 150 149 147 i0 2 i1 4 i2 6 i3 8 i4 10 i5 12 i6 14 i7 16 i8 18 i9 20 i10 22 i11 24 l0 26 l1 28 l2 30 l3 32 l4 34 l5 36 l6 38 l7 40 l8 42 l9 44 l10 46 l11 48 l12 50 l13 52 l14 54 l15 56 l16 58 l17 60 l18 62 l19 64 l20 66 o0 71 c model: CEGAR-TEST3 i0 IN1 2 i1 IN2 4 i2 ODD1-IN2 6 i3 ODD1-IN4 8 i4 ODD1-IN5 10 i5 ODD2-IN2 12 i6 ODD2-IN4 14 i7 ODD2-IN5 16 i8 COUNTER0-CIN 18 i9 COUNTER1-CIN 20 i10 COUNTER2-CIN 22 i11 COUNTER3-CIN 24 DISJ1 26 next: NEXTL0 103 DISJ2 28 next: NEXTL1 88 DISJ3 30 next: NEXTL2 74 LATCH1 32 next: NEXTLATCH1 134 LATCH2 34 next: (NOT IN1) 3 LATCH3 36 next: IN2 4 LATCH4 38 next: NEXTLATCH4 122 ODD1-L2 40 next: ODD1-IN2 6 ODD1-L4 42 next: ODD1-IN4 8 ODD1-L5 44 next: ODD1-IN5 10 ODD2-L2 46 next: ODD2-IN2 12 ODD2-L4 48 next: ODD2-IN4 14 ODD2-L5 50 next: ODD2-IN5 16 COUNTER0-L0 52 next: COUNTER0-NEXT0 108 COUNTER0-L1 54 next: COUNTER0-NEXT1 114 COUNTER1-L0 56 next: COUNTER1-NEXT0 120 COUNTER1-L1 58 next: COUNTER1-NEXT1 126 COUNTER2-L0 60 next: COUNTER2-NEXT0 132 COUNTER2-L1 62 next: COUNTER2-NEXT1 138 COUNTER3-L0 64 next: COUNTER3-NEXT0 144 COUNTER3-L1 66 next: COUNTER3-NEXT1 150 o0 TOP-OR 71 QCHECK/aiger-model/examples/cegar-test3.laig000644 000765 000024 00000004410 12332735360 021733 0ustar00fspedalistaff000000 000000 (model cegar-test3 (latch disj1 nextl0) (latch disj2 nextl1) (latch disj3 nextl2) (or-gate ((d1 disj1) (d2 disj2)) ((val or1))) (or-gate ((d1 or1) (d2 disj3)) ((val top-or))) (output top-or) (defblock or-gate (:params d1 d2 :outputs (val (not tmp)) :locals tmp) (and tmp (not d1) (not d2))) (defblock counter (:params :outputs (val carry-out) :locals cin l0 l1 c0 none0 next0 carry-out none1 next1 ) (input cin) (latch l0 next0) (and c0 l0 cin) ; carry out of first bit (and none0 (not l0) (not cin)) (and next0 (not none0) (not c0)) ; cin ^ l0 (latch l1 next1) (and carry-out l1 c0) (and none1 (not l1) (not c0)) (and next1 (not none1) (not carry-out))) (input in1) (latch latch1 nextlatch1) (latch latch2 (not in1)) (input in2) (latch latch3 in2) (latch latch4 nextlatch4) (oddball-function odd1 ((l1 latch1)(l3 latch3)) ((val nextl2))) (oddball-function odd2 ((l1 latch4) (l3 orval)) ((val nextl1))) (or-gate or3 ((d1 latch1)(d2 count-end)) ((val orval))) (defblock oddball-function (:params l1 l3 :outputs (val top-and) :locals in2 in4 in5 l2 l4 l5 pair top-and pair1 pair2 pair3 none12 no-pair) (input in2) (latch l2 in2) (input in4) (latch l4 in4) (input in5) (latch l5 in5) (and pair l1 l2) (and top-and pair (not no-pair)) (and pair1 l3 l4) (and pair2 l3 l5) (and pair3 l4 l5) (and none12 (not pair1) (not pair2)) (and no-pair none12 (not pair3)) ) (or-gate disj1 ((d1 counter0-out) (d2 latch2)) ((val nextl0))) (counter counter0 () ((val counter0-out))) (counter counter1 () ((val nextlatch4))) (counter counter2 () ((val nextlatch1))) (counter counter3 () ((val count-end))) ) QCHECK/aiger-model/examples/fcs5000-lat.laig000644 000765 000024 00000015331 12332735360 021454 0ustar00fspedalistaff000000 000000 (model fcs5000-lat (defblock or-gate (:params x y :locals gate :outputs (val (not gate))) (and gate (not x) (not y))) (defblock no-others (:params o1 o2 o3 :locals tmp1 tmp2 :outputs (val tmp1)) (and tmp1 (not o1) tmp2) (and tmp2 (not o2) (not o3))) (defblock persist (:params now o1 o2 o3 :locals persist no-others :outputs (persist persist)) (no-others persist-no-others ((o1 o1) (o2 o2) (o3 o3)) ((val no-others))) (and persist now no-others)) (defblock rising-edge (:params now last :locals rising :outputs (val rising)) (and rising now (not last))) (defblock only-once (:params input :outputs (val one-shot) :locals one-shot tmp l1) (latch l1 input) ; will rise and fall (latch one-shot one-shot-val) (or-gate tmp ((x one-shot) (y l1)) ((val one-shot-val)))) (only-once powering-up ((input power-up-in)) ((val power))) (latch chg-coupled-side chg-coupled-side-in) (latch hdg-switch hdg-switch-in) (latch hdg-switch-not-vappr no-vappr-check) (latch sync-switch sync-switch-in) (latch ga-switch ga-switch-in) (latch vga vga-switch-in) (latch not-vga (not vga-switch-in)) (latch lappr-capture lappr-captured) ;; change so that lapp-captured only when ;; Vertical Approach is already captured. (and lappr-captured lappr-capture-in vappr) (and no-vappr-check hdg-switch-in (not vappr)) (input power-up-in) (input chg-coupled-side-in) (input hdg-switch-in) (input sync-switch-in) (input ga-switch-in) (input vga-switch-in) (input lappr-capture-in) ;; add logic to check for VAPPR... ;; this is a little bit made up.... (latch vappr vappr-check) (input vappr1) (input vappr2) (input vappr3) ;; vappr inputs must be positive for three counts... (latch v11 vappr1) (latch v12 vappr2) (latch v13 vappr3) (latch v21 v11) (latch v22 v12) (latch v23 v13) (latch v31 v21) (latch v32 v22) (latch v33 v23) (and vappr-check v11 vc2) (and vc2 v12 vc3) (and vc3 v13 vc4) (and vc4 v21 vc5) (and vc5 v22 vc6) (and vc6 v23 vc7) (and vc7 v31 vc8) (and vc8 v32 v33) (latch last-power power) (latch last-chg-coupled-side chg-coupled-side) (latch last-hdg-switch hdg-switch) (latch last-hdg-switch-not-vappr hdg-switch-not-vappr) (latch last-sync-switch sync-switch) (latch last-ga-switch ga-switch) (latch last-vga vga) (latch last-not-vga not-vga) (latch last-lappr-capture lappr-capture) (latch roll roll-enable) (latch hdg hdg-enable) (latch lappr lappr-enable) (latch lga lga-enable) ;; rising edges (rising-edge power-up ((now power) (last last-power)) ((val power-up-rising))) (rising-edge chg-coupled-side ((now chg-coupled-side) (last last-chg-coupled-side)) ((val chg-coupled-side-rising))) (rising-edge hdg-switch ((now hdg-switch) (last last-hdg-switch)) ((val hdg-switch-rising))) (rising-edge hdg-switch-not-vappr ((now hdg-switch-not-vappr) (last last-hdg-switch-not-vappr)) ((val hdg-switch-not-vappr-rising))) (rising-edge sync-switch ((now sync-switch) (last last-sync-switch)) ((val sync-switch-rising))) (rising-edge ga-switch ((now ga-switch) (last last-ga-switch)) ((val ga-switch-rising))) (rising-edge vga ((now vga) (last last-vga)) ((val vga-rising))) (rising-edge not-vga ((now not-vga) (last last-not-vga)) ((val not-vga-rising))) (rising-edge lappr-capture ((now lappr-capture) (last last-lappr-capture)) ((val lappr-capture-rising))) ;; roll enable logic (or-gate roll-enable ((x roll-persist) (y roll-enable-on)) ((val roll-enable))) (persist roll-persist ((now roll) (o1 hdg-enable-on) (o2 lappr-enable-on) (o3 lga-enable-on)) ((persist roll-persist))) (or-gate ((x reo1) (y power-up-rising)) ((val roll-enable-on))) (and reo1 chg-coupled-side-rising reo2) (and reo2 hdg-switch-rising reo3) (and reo3 sync-switch-rising reo4) (and reo4 (not roll) not-vga-rising) ;; hdg enable logic (or-gate hdg-enable ((x hdg-persist) (y hdg-enable-on)) ((val hdg-enable))) (persist hdg-persist ((now hdg) (o1 roll-enable-on) (o2 lappr-enable-on) (o3 lga-enable-on)) ((persist hdg-persist))) (and hdg-enable-on (not power-up-rising) heo1) (and heo1 hdg-switch-rising heo2) (and heo2 hdg-switch-not-vappr-rising heo3) (and heo3 power heo4) (and heo4 (not hdg) (not roll-enable-on)) ; ROLL takes precedence over HDG. ;; lappr-enable logic (or-gate lappr-enable ((x lappr-persist) (y lappr-enable-on)) ((val lappr-enable))) (persist lappr-persist ((now lappr) (o1 roll-enable-on) (o2 hdg-enable-on) (o3 lga-enable-on)) ((persist lappr-persist))) (and lappr-enable-on (not power-up-rising) laeo1) (and laeo1 (not lappr) laeo2) (and laeo2 power laeo3) (and laeo3 lappr-capture-rising laeo4) ;; the next two capture heading taking precedence over LAPPR. (and laeo4 (not sync-switch-rising) laeo5) (and laeo5 (not hdg-switch-rising) laeo6) (and laeo6 vappr (not ga-switch-rising)) ; go-around breaks out of lateral approach ;; lga-enable logic (or-gate lga-enable ((x lga-persist) (y lga-enable-on)) ((val lga-enable))) (persist lga-persist ((now lga) (o1 roll-enable-on) (o2 hdg-enable-on) (o3 lappr-enable-on)) ((persist lga-persist))) (and lga-enable-on (not power-up-rising) leo1) (and leo1 ga-switch-rising leo2) (and leo2 vga-rising leo3) (and leo3 (not lga) leo4) (and leo4 power (not hdg-enable-on)) ; HDG wins over LGA according to the paper. ;; FIXME: LAPPR should be required to be the previous state... (or-gate top-o ((x pair1) (y bad1)) ((val bad))) (and pair1 roll hdg) (or-gate ((x pair2) (y bad2)) ((val bad1))) (and pair2 roll lappr) (or-gate ((x pair3) (y bad3)) ((val bad2))) (and pair3 roll lga) (or-gate ((x pair4) (y bad4)) ((val bad3))) (and pair4 hdg lappr) (or-gate ((x pair5) (y pair6)) ((val bad4))) (and pair5 hdg lga) (and pair6 lappr lga) ;; violation of safety property. (output bad)) QCHECK/aiger-model/examples/fcs5000-lat2.laig000644 000765 000024 00000016626 12332735360 021546 0ustar00fspedalistaff000000 000000 (model fcs5000-lat (defblock or-gate (:params x y :locals gate :outputs (val (not gate))) (and gate (not x) (not y))) (defblock no-others (:params o1 o2 o3 :locals tmp1 tmp2 :outputs (val tmp1)) (and tmp1 (not o1) tmp2) (and tmp2 (not o2) (not o3))) (defblock persist (:params now o1 o2 o3 :locals persist no-others :outputs (persist persist)) (no-others persist-no-others ((o1 o1) (o2 o2) (o3 o3)) ((val no-others))) (and persist now no-others)) (defblock rising-edge (:params now last :locals rising :outputs (val rising)) (and rising now (not last))) (defblock only-once (:params input :outputs (val one-shot) :locals one-shot tmp l1) (latch l1 input) ; will rise and fall (latch one-shot one-shot-val) (or-gate tmp ((x one-shot) (y l1)) ((val one-shot-val)))) (only-once powering-up ((input power-up-in)) ((val power))) (latch chg-coupled-side chg-coupled-side-in) (latch hdg-switch hdg-switch-in) (latch hdg-switch-not-vappr no-vappr-check) (latch sync-switch sync-switch-in) (latch ga-switch ga-switch-in) (latch vga go-around-on) (or-gate vga-manual-or-auto ((x vga-switch-in)(y (not vappr))) ((val go-around-on))) (latch not-vga (not vga-switch-in)) (latch lappr-capture lappr-captured) ;; change so that lapp-captured only when ;; Vertical Approach is already captured. (and lappr-captured lappr-capture-in vappr) (and no-vappr-check hdg-switch-in (not vappr)) (input power-up-in) (input chg-coupled-side-in) (input hdg-switch-in) (input sync-switch-in) (input ga-switch-in) (input vga-switch-in) (input lappr-capture-in) ;; add logic to check for VAPPR... ;; this is a little bit made up.... (latch vappr vappr-check) (input vappr1) (input vappr2) (input vappr3) ;; vappr inputs must be positive for three counts... (latch v11 vappr1) (latch v12 vappr2) (latch v13 vappr3) (latch v21 v11) (latch v22 v12) (latch v23 v13) (latch v31 v21) (latch v32 v22) (latch v33 v23) (and vappr-check v11 vc2) (and vc2 v12 vc3) (and vc3 v13 vc4) (and vc4 v21 vc5) (and vc5 v22 vc6) (and vc6 v23 vc7) (and vc7 v31 vc8) (and vc8 v32 v33) (latch last-power power) (latch last-chg-coupled-side chg-coupled-side) (latch last-hdg-switch hdg-switch) (latch last-hdg-switch-not-vappr hdg-switch-not-vappr) (latch last-sync-switch sync-switch) (latch last-ga-switch ga-switch) (latch last-vga vga) (latch last-not-vga not-vga) (latch last-lappr-capture lappr-capture) (latch roll roll-enable) (latch hdg hdg-enable) (latch lappr lappr-enable) (latch lga lga-enable) ;; rising edges (rising-edge power-up ((now power) (last last-power)) ((val power-up-rising))) (rising-edge chg-coupled-side ((now chg-coupled-side) (last last-chg-coupled-side)) ((val chg-coupled-side-rising))) (rising-edge hdg-switch ((now hdg-switch) (last last-hdg-switch)) ((val hdg-switch-rising))) (rising-edge hdg-switch-not-vappr ((now hdg-switch-not-vappr) (last last-hdg-switch-not-vappr)) ((val hdg-switch-not-vappr-rising))) (rising-edge sync-switch ((now sync-switch) (last last-sync-switch)) ((val sync-switch-rising))) (rising-edge ga-switch ((now ga-switch) (last last-ga-switch)) ((val ga-switch-rising))) (rising-edge vga ((now vga) (last last-vga)) ((val vga-rising))) (rising-edge not-vga ((now not-vga) (last last-not-vga)) ((val not-vga-rising))) (rising-edge lappr-capture ((now lappr-capture) (last last-lappr-capture)) ((val lappr-capture-rising))) ;; roll enable logic (or-gate roll-enable ((x roll-persist) (y roll-enable-on)) ((val roll-enable))) (persist roll-persist ((now roll) (o1 hdg-enable-on) (o2 lappr-enable-on) (o3 lga-enable-on)) ((persist roll-persist))) (or-gate ((x reo1) (y power-up-rising)) ((val roll-enable-on))) (and reo1 (not roll) reo2) ;don't change if we're already in ROLL (and reo2 not-vga-rising reo3) ; don't change if VGA rising (and reo3 (not lappr) reodisj) ; don't jump directly to roll from lateral approach -- do LGA ;; disjunctive reasons to switch (or-gate ((x chg-coupled-side-rising) (y reodisj1)) ((val reodisj))) (or-gate ((x sync-switch-rising) (y reodisj2)) ((val reodisj1))) (and reodisj2 hdg-switch-rising hdg) ; if HDG switch and in HDG mode ;; hdg enable logic (or-gate hdg-enable ((x hdg-persist) (y hdg-enable-on)) ((val hdg-enable))) (persist hdg-persist ((now hdg) (o1 roll-enable-on) (o2 lappr-enable-on) (o3 lga-enable-on)) ((persist hdg-persist))) (and hdg-enable-on (not power-up-rising) heo1) (and heo1 hdg-switch-rising heo2) (and heo2 hdg-switch-not-vappr-rising heo3) (and heo3 power heo4) (and heo4 (not hdg) heo5) (and heo5 (not roll-enable-on) prev-state-for-hdg) ; ROLL takes precedence over HDG. (or-gate prev-state-for-hdg-disj ((x roll) (y lga)) ((val prev-state-for-hdg))) ;; lappr-enable logic (or-gate lappr-enable ((x lappr-persist) (y lappr-enable-on)) ((val lappr-enable))) (persist lappr-persist ((now lappr) (o1 roll-enable-on) (o2 hdg-enable-on) (o3 lga-enable-on)) ((persist lappr-persist))) (and lappr-enable-on (not power-up-rising) laeo1) (and laeo1 (not lappr) laeo2) (and laeo2 power laeo3) (and laeo3 lappr-capture-rising laeo4) ;; the next two capture heading taking precedence over LAPPR. (and laeo4 (not sync-switch-rising) laeo5) (and laeo5 (not hdg-switch-rising) laeo6) (and laeo6 vappr laeo7) (and laeo7 (not ga-switch-rising) ; go-around breaks out of lateral approach (not chg-coupled-side-rising)) ; chg-coupled-side-rising puts us into ROLL instead ;; lga-enable logic (or-gate lga-enable ((x lga-persist) (y lga-enable-on)) ((val lga-enable))) (persist lga-persist ((now lga) (o1 roll-enable-on) (o2 hdg-enable-on) (o3 lappr-enable-on)) ((persist lga-persist))) (and lga-enable-on (not power-up-rising) leo1) (and leo1 ga-switch-rising leo2) (and leo2 vga-rising leo3) (and leo3 (not lga) leo4) (and leo4 power leo5) (and leo5 (not hdg-enable-on) ; HDG wins over LGA according to the paper. lappr) ; must be in an approach to do a go-around (or-gate top-o ((x pair1) (y bad1)) ((val bad))) (and pair1 roll hdg) (or-gate ((x pair2) (y bad2)) ((val bad1))) (and pair2 roll lappr) (or-gate ((x pair3) (y bad3)) ((val bad2))) (and pair3 roll lga) (or-gate ((x pair4) (y bad4)) ((val bad3))) (and pair4 hdg lappr) (or-gate ((x pair5) (y pair6)) ((val bad4))) (and pair5 hdg lga) (and pair6 lappr lga) ;; violation of safety property. (output bad)) QCHECK/aiger-model/examples/fcs5000-lat3.laig000644 000765 000024 00000021526 12332735360 021542 0ustar00fspedalistaff000000 000000 ;;; Made a number of modifications in order to get more interesting ILPs. ;;; * Instead of having VAPPR require latching three sets of three acceptable values ;;; (i.e., three clock cycles of all three on), instead I used a two-of-three ;;; criterion. That was intended to provide more variation while still being realistic. ;;; * Instead of using the raw GO-AROUND-ON as the value for VGA (allowing either loss of ;;; VAPPR or VGA-switch-in), I now latch the value. I don't think that this makes much difference, ;;; but it allows another cycle of abstraction and refinement. ;;; * Remove the special LAST-NOT-VGA latch -- that will, if anything, make the ILPs *less* ;;; interesting as it hides interactions. ;;; * Replace NOT-VGA with the more primitive (NOT VGA); again this should reveal shared structure ;;; that latching separately will obscure. Latching separately is unrealistic, anyway. ;;; * Restructured the ROLL turn-on conditions to be more clear and made them disjunctive. I believe ;;; this to be more realistic in addition to the fact that it SHOULD make for better ILPs. (model fcs5000-lat3 (defblock alias (:params to :outputs (from to))) (defblock or-gate (:params x y :locals gate :outputs (val (not gate))) (and gate (not x) (not y))) (defblock no-others (:params o1 o2 o3 :locals tmp1 tmp2 :outputs (val tmp1)) (and tmp1 (not o1) tmp2) (and tmp2 (not o2) (not o3))) (defblock persist (:params now o1 o2 o3 :locals persist no-others :outputs (persist persist)) (no-others persist-no-others ((o1 o1) (o2 o2) (o3 o3)) ((val no-others))) (and persist now no-others)) (defblock rising-edge (:params now last :locals rising :outputs (val rising)) (and rising now (not last))) (defblock only-once (:params input :outputs (val one-shot) :locals one-shot tmp l1) (latch l1 input) ; will rise and fall (latch one-shot one-shot-val) (or-gate tmp ((x one-shot) (y l1)) ((val one-shot-val)))) (defblock at-least-two ( :params x y z :outputs (val at-least-two)) (and pair1 x y) (and pair2 x z) (and pair3 y z) (or-gate d1 ((x pair1) (y pair2)) ((val x1out))) (or-gate d2 ((x x1out) (y pair3)) ((val at-least-two)))) (only-once powering-up ((input power-up-in)) ((val power))) (latch chg-coupled-side chg-coupled-side-in) (latch hdg-switch hdg-switch-in) (latch hdg-switch-not-vappr no-vappr-check) (latch sync-switch sync-switch-in) (latch ga-switch ga-switch-in) (or-gate vga-manual-or-auto ((x vga-switch-in)(y (not vappr))) ((val go-around-on))) (latch vga go-around-on) ;; (latch not-vga (not vga-switch-in)) (latch lappr-capture lappr-captured) ;; change so that lapp-captured only when ;; Vertical Approach is already captured. (and lappr-captured lappr-capture-in vappr) (and no-vappr-check hdg-switch-in (not vappr)) (input power-up-in) (input chg-coupled-side-in) (input hdg-switch-in) (input sync-switch-in) (input ga-switch-in) (input vga-switch-in) (input lappr-capture-in) ;; add logic to check for VAPPR... ;; (latch vappr vappr-check) (alias ((to vappr-check)) ((from vappr))) (input vappr1) (input vappr2) (input vappr3) ;; vappr inputs must be positive for three counts... (latch v11 vappr1) (latch v12 vappr2) (latch v13 vappr3) (latch v21 v11) (latch v22 v12) (latch v23 v13) (latch v31 v21) (latch v32 v22) (latch v33 v23) ;; each tick we must have two of three to get vappr... (and vappr-check vc-pair1 vc2) (and vc2 vc-pair2 vc-pair3) (at-least-two ((x v11) (y v12) (z v13)) ((val vc-pair1))) (at-least-two ((x v21) (y v22) (z v23)) ((val vc-pair2))) (at-least-two ((x v31) (y v32) (z v33)) ((val vc-pair3))) (and vappr-check v11 vc2) (and vc2 v12 vc3) (and vc3 v13 vc4) (and vc4 v21 vc5) (and vc5 v22 vc6) (and vc6 v23 vc7) (and vc7 v31 vc8) (and vc8 v32 v33) (latch last-power power) (latch last-chg-coupled-side chg-coupled-side) (latch last-hdg-switch hdg-switch) (latch last-hdg-switch-not-vappr hdg-switch-not-vappr) (latch last-sync-switch sync-switch) (latch last-ga-switch ga-switch) (latch last-vga vga) (alias ((to (not last-vga))) ((from last-not-vga))) (latch last-lappr-capture lappr-capture) (latch roll roll-enable) (latch hdg hdg-enable) (latch lappr lappr-enable) (latch lga lga-enable) ;; rising edges (rising-edge power-up ((now power) (last last-power)) ((val power-up-rising))) (rising-edge chg-coupled-side ((now chg-coupled-side) (last last-chg-coupled-side)) ((val chg-coupled-side-rising))) (rising-edge hdg-switch ((now hdg-switch) (last last-hdg-switch)) ((val hdg-switch-rising))) (rising-edge hdg-switch-not-vappr ((now hdg-switch-not-vappr) (last last-hdg-switch-not-vappr)) ((val hdg-switch-not-vappr-rising))) (rising-edge sync-switch ((now sync-switch) (last last-sync-switch)) ((val sync-switch-rising))) (rising-edge ga-switch ((now ga-switch) (last last-ga-switch)) ((val ga-switch-rising))) (rising-edge vga ((now vga) (last last-vga)) ((val vga-rising))) (rising-edge not-vga ((now (not vga)) (last (not last-vga))) ((val not-vga-rising))) (rising-edge lappr-capture ((now lappr-capture) (last last-lappr-capture)) ((val lappr-capture-rising))) ;; roll enable logic (or-gate roll-enable ((x roll-persist) (y roll-enable-on)) ((val roll-enable))) (persist roll-persist ((now roll) (o1 hdg-enable-on) (o2 lappr-enable-on) (o3 lga-enable-on)) ((persist roll-persist))) ;; roll enable goes on when the system boots (or-gate ((x reo1) (y power-up-rising)) ((val roll-enable-on))) ;; or when some conditions hold and we switch it on... (and reo1 roll-triggers roll-conditions) (and roll-conditions (not roll) not-vga-rising) (or-gate roll-triggers1 ((x chg-coupled-side-rising) (y rtd1)) ((val roll-triggers))) (or-gate roll-triggers2 ((x hdg-switch-rising) (y sync-switch-rising)) ((val rtd1))) ;; hdg enable logic (or-gate hdg-enable ((x hdg-persist) (y hdg-enable-on)) ((val hdg-enable))) (persist hdg-persist ((now hdg) (o1 roll-enable-on) (o2 lappr-enable-on) (o3 lga-enable-on)) ((persist hdg-persist))) (and hdg-enable-on (not power-up-rising) heo1) (and heo1 hdg-switch-rising heo2) (and heo2 hdg-switch-not-vappr-rising heo3) (and heo3 power heo4) (and heo4 (not hdg) (not roll-enable-on)) ; ROLL takes precedence over HDG. ;; lappr-enable logic (or-gate lappr-enable ((x lappr-persist) (y lappr-enable-on)) ((val lappr-enable))) (persist lappr-persist ((now lappr) (o1 roll-enable-on) (o2 hdg-enable-on) (o3 lga-enable-on)) ((persist lappr-persist))) (and lappr-enable-on (not power-up-rising) laeo1) (and laeo1 (not lappr) laeo2) (and laeo2 power laeo3) (and laeo3 lappr-capture-rising laeo4) ;; the next two capture heading taking precedence over LAPPR. (and laeo4 (not sync-switch-rising) laeo5) (and laeo5 (not hdg-switch-rising) laeo6) (and laeo6 vappr (not ga-switch-rising)) ; go-around breaks out of lateral approach ;; lga-enable logic (or-gate lga-enable ((x lga-persist) (y lga-enable-on)) ((val lga-enable))) (persist lga-persist ((now lga) (o1 roll-enable-on) (o2 hdg-enable-on) (o3 lappr-enable-on)) ((persist lga-persist))) (and lga-enable-on (not power-up-rising) leo1) (and leo1 ga-switch-rising leo2) (and leo2 vga-rising leo3) (and leo3 (not lga) leo4) (and leo4 power (not hdg-enable-on)) ; HDG wins over LGA according to the paper. ;; FIXME: LAPPR should be required to be the previous state... (or-gate top-o ((x pair1) (y bad1)) ((val bad))) (and pair1 roll hdg) (or-gate ((x pair2) (y bad2)) ((val bad1))) (and pair2 roll lappr) (or-gate ((x pair3) (y bad3)) ((val bad2))) (and pair3 roll lga) (or-gate ((x pair4) (y bad4)) ((val bad3))) (and pair4 hdg lappr) (or-gate ((x pair5) (y pair6)) ((val bad4))) (and pair5 hdg lga) (and pair6 lappr lga) ;; violation of safety property. (output bad)) QCHECK/aiger-model/examples/inverter.aag000644 000765 000024 00000000104 12332735360 021260 0ustar00fspedalistaff000000 000000 aag 1 1 0 1 0 2 3 i0 2 o0 3 c model: INVERTER i0 I0 2 o0 (NOT I0) 3 QCHECK/aiger-model/examples/inverter.laig000644 000765 000024 00000000062 12332735360 021447 0ustar00fspedalistaff000000 000000 (model inverter (input i0) (output (not i0))) QCHECK/aiger-model/examples/new-try.laig000644 000765 000024 00000023501 12332735360 021221 0ustar00fspedalistaff000000 000000 (model new-try ;; (defblock alias (:params to :outputs (from to))) (defblock or-gate (:params x y :locals gate :outputs (val (not gate))) (and gate (not x) (not y))) ;; (defblock no-others (:params o1 o2 o3 ;; :locals tmp1 tmp2 ;; :outputs (val tmp1)) ;; (and tmp1 (not o1) tmp2) ;; (and tmp2 (not o2) (not o3))) ;; (defblock persist (:params now o1 o2 o3 ;; :locals persist no-others ;; :outputs (persist persist)) ;; (no-others persist-no-others ((o1 o1) (o2 o2) (o3 o3)) ((val no-others))) ;; (and persist now no-others)) ;; (defblock rising-edge (:params now last ;; :locals rising ;; :outputs (val rising)) ;; (and rising now (not last))) (defblock only-once (:params input :outputs (val one-shot) :locals one-shot tmp l1) (latch l1 input) ; will rise and fall (latch one-shot one-shot-val) (or-gate tmp ((x one-shot) (y l1)) ((val one-shot-val)))) ;; (only-once powering-up ((input power-up-in)) ((val power))) ;; (latch chg-coupled-side chg-coupled-side-in) ;; (latch hdg-switch hdg-switch-in) ;; (latch hdg-switch-not-vappr no-vappr-check) ;; (latch sync-switch sync-switch-in) ;; (latch ga-switch ga-switch-in) ;; (alias ((to go-around-on)) ((from vga))) ;; (or-gate vga-manual-or-auto ((x vga-switch-in)(y (not vappr))) ((val go-around-on))) ;; ;; (latch vga vga-switch-in) ;; (latch not-vga (not vga-switch-in)) ;; (latch lappr-capture lappr-captured) ;; ;; change so that lapp-captured only when ;; ;; Vertical Approach is already captured. ;; (and lappr-captured lappr-capture-in vappr) ;; (and no-vappr-check hdg-switch-in (not vappr)) ;; (input power-up-in) ;; (input chg-coupled-side-in) ;; (input hdg-switch-in) ;; (input sync-switch-in) ;; (input ga-switch-in) ;; (input vga-switch-in) ;; (input lappr-capture-in) ;; ;; add logic to check for VAPPR... ;; ;; this is a little bit made up.... ;; ;;(latch vappr vappr-check) ;; (alias ((to vappr-check)) ((from vappr))) ;; (input vappr1) ;; (input vappr2) ;; (input vappr3) ;; (input vappr4) ;; (input vappr5) ;; (input vappr6) ;; ;; vappr inputs must be positive for three counts... ;; (latch v11 vappr1) ;; (latch v12 vappr2) ;; (latch v13 vappr3) ;; (latch v21 v11) ;; (latch v22 v12) ;; (latch v23 v13) ;; (latch v31 vappr4) ;; (latch v32 vappr5) ;; (latch v33 vappr6) ;; (and vappr-check v11 vc2) ;; (and vc2 v12 vc3) ;; (and vc3 v13 vc4) ;; (and vc4 v21 vc5) ;; (and vc5 v22 vc6) ;; (and vc6 v23 vc7) ;; (and vc7 v31 vc8) ;; (and vc8 v32 v33) ;; (latch last-power power) ;; (latch last-chg-coupled-side chg-coupled-side) ;; (latch last-hdg-switch hdg-switch) ;; (latch last-hdg-switch-not-vappr hdg-switch-not-vappr) ;; (latch last-sync-switch sync-switch) ;; (latch last-ga-switch ga-switch) ;; (latch last-vga vga) ;; (latch last-not-vga not-vga) ;; (latch last-lappr-capture lappr-capture) ;; (latch roll roll-enable) ;; (latch hdg hdg-enable) ;; (latch lappr lappr-enable) ;; (latch lga lga-enable) ;; ;; rising edges ;; (rising-edge power-up ((now power) (last last-power)) ((val power-up-rising))) ;; (rising-edge chg-coupled-side ((now chg-coupled-side) (last last-chg-coupled-side)) ;; ((val chg-coupled-side-rising))) ;; (rising-edge hdg-switch ((now hdg-switch) (last last-hdg-switch)) ((val hdg-switch-rising))) ;; (rising-edge hdg-switch-not-vappr ((now hdg-switch-not-vappr) (last last-hdg-switch-not-vappr)) ;; ((val hdg-switch-not-vappr-rising))) ;; (rising-edge sync-switch ((now sync-switch) (last last-sync-switch)) ((val sync-switch-rising))) ;; (rising-edge ga-switch ((now ga-switch) (last last-ga-switch)) ((val ga-switch-rising))) ;; (rising-edge vga ((now vga) (last last-vga)) ((val vga-rising))) ;; (rising-edge not-vga ((now not-vga) (last last-not-vga)) ((val not-vga-rising))) ;; (rising-edge lappr-capture ((now lappr-capture) (last last-lappr-capture)) ((val lappr-capture-rising))) ;; ;; roll enable logic ;; (or-gate roll-enable ((x roll-persist) (y roll-enable-on)) ((val roll-enable))) ;; (persist roll-persist ((now roll) (o1 hdg-enable-on) (o2 lappr-enable-on) (o3 lga-enable-on)) ((persist roll-persist))) ;; (or-gate ((x reo1) (y power-up-rising)) ((val roll-enable-on))) ;; (and reo1 chg-coupled-side-rising reo2) ;; (and reo2 hdg-switch-rising reo3) ;; (and reo3 sync-switch-rising reo4) ;; (and reo4 (not roll) not-vga-rising) ;; ;; hdg enable logic ;; (or-gate hdg-enable ((x hdg-persist) (y hdg-enable-on)) ((val hdg-enable))) ;; (persist hdg-persist ((now hdg) (o1 roll-enable-on) (o2 lappr-enable-on) (o3 lga-enable-on)) ((persist hdg-persist))) ;; (and hdg-enable-on (not power-up-rising) heo1) ;; (and heo1 hdg-switch-rising heo2) ;; (and heo2 hdg-switch-not-vappr-rising heo3) ;; (and heo3 power heo4) ;; (and heo4 (not hdg) (not roll-enable-on)) ; ROLL takes precedence over HDG. ;; ;; lappr-enable logic ;; (or-gate lappr-enable ((x lappr-persist) (y lappr-enable-on)) ((val lappr-enable))) ;; (persist lappr-persist ((now lappr) (o1 vappr) (o2 hdg-enable-on) (o3 lga-enable-on)) ((persist lappr-persist))) ;; (and lappr-enable-on (not power-up-rising) laeo1) ;; (and laeo1 (not lappr) laeo2) ;; (and laeo2 power laeo3) ;; (and laeo3 lappr-capture-rising laeo4) ;; ;; the next two capture heading taking precedence over LAPPR. ;; (and laeo4 (not sync-switch-rising) laeo5) ;; (and laeo5 (not hdg-switch-rising) laeo6) ;; (and laeo6 vappr (not ga-switch-rising)) ; go-around breaks out of lateral approach ;; ;; lga-enable logic ;; (or-gate lga-enable ((x lga-persist) (y lga-enable-on)) ((val lga-enable))) ;; (persist lga-persist ((now lga) (o1 roll-enable-on) (o2 hdg-enable-on) (o3 lappr-enable-on)) ((persist lga-persist))) ;; (and lga-enable-on (not power-up-rising) leo1) ;; (and leo1 ga-switch-rising leo2) ;; (and leo2 vga-rising leo3) ;; (and leo3 (not lga) leo4) ;; (and leo4 power (not hdg-enable-on)) ; HDG wins over LGA according to the paper. ;; ;; FIXME: LAPPR should be required to be the previous state... ;; (or-gate top-o ((x pair1) (y bad1)) ((val bad))) ;; (and pair1 roll hdg) ;; (or-gate ((x pair2) (y bad2)) ((val bad1))) ;; (and pair2 roll lappr) ;; (or-gate ((x pair3) (y bad3)) ((val bad2))) ;; (and pair3 roll lga) ;; (or-gate ((x pair4) (y bad4)) ((val bad3))) ;; (and pair4 hdg lappr) ;; (or-gate ((x pair5) (y pair6)) ((val bad4))) ;; (and pair5 hdg lga) ;; (and pair6 lappr lga) ;; ground approach transmission. this is the true state (input GA) ;; when its on, (only-once ga-state ((input GA)) ((val true-ga-val))) (input ga-error) (only-once ga-sense1 ((input ga-sense1)) ((val ga-sense1-latch))) (only-once ga-sense2 ((input ga-sense2)) ((val ga-sense2-latch))) (only-once ga-sense3 ((input ga-sense3)) ((val ga-sense3-latch))) ;; need to latch three values... (and ga-sense1 true-ga-val (not ga-error)) (and ga-sense2 ga-sense1-latch ga-good) (and ga-good true-ga-val (not ga-error)) (and ga-sense3 ga-sense2-latch ga-good) (only-once ga-error1 ((input ga-error)) ((val one-ga-error))) (only-once ga-error2 ((input ga-error2)) ((val two-ga-errors))) (and ga-error2 one-ga-error ga-error) (input input1) (input input2) (input input3) (input input4) (latch common1 input1) (latch common2 input2) (latch common3 input3) (latch common4 input4) (input ground-approach-switch) (input ground-approach-disable-switch) (only-once ground-approach-disablement ((input ground-approach-disable-switch)) ((val ground-approach-disabled))) ;; we begin ground approach one tick after we have securely sensed it ;; and the pilot engages the switch (and engage-ground-approach ground-approach-switch-on ga-sense3-latch) (and ground-approach-switch-on ground-approach-switch (not ground-approach-disabled)) ;; auto-pilot (input autopilot-switch) (only-once auto-pilot-engagement ((input autopilot-switch)) ((val autopilot-switch-on))) ;; (and autopilot-on autopilot-switch-on (not true-GA-val)) (latch mode1-specific engage-ground-approach) (latch mode2-specific autopilot-on) (and ground-approach-on all-common mode1-specific) (and level-flight-on all-common mode2-specific) (and all-common ac1 ac2) (and ac1 common1 common2) (and ac2 common3 common4) (latch ground-approach ground-approach-on) (latch level-flight level-flight-on) ;; this captures conditions that we consider cannot happen in our model. (latch valid (not ga-error2)) (and bad ground-approach level-flight) ;; we reject model failures (and valid-bad bad valid) ;; violation of safety property. (output valid-bad)) QCHECK/aiger-model/examples/or-gate.aag000644 000765 000024 00000000135 12332735360 020764 0ustar00fspedalistaff000000 000000 aag 3 2 0 1 1 2 4 7 6 3 5 i0 2 i1 4 o0 7 c model: OR-GATE i0 D0 2 i1 D1 4 o0 (NOT AND-NOT) 7 QCHECK/aiger-model/examples/or-gate.laig000644 000765 000024 00000000143 12332735360 021147 0ustar00fspedalistaff000000 000000 (model or-gate (input d0) (input d1) (output (not and-not)) (and and-not (not d0) (not d1))) QCHECK/aiger-model/examples/toggle-flip-flop.aag000644 000765 000024 00000000147 12332735360 022600 0ustar00fspedalistaff000000 000000 aag 1 0 1 2 0 2 3 2 3 l0 2 o0 2 o1 3 c model: TOGGLE-FLIP-FLOP L 2 next: (NOT L) 3 o0 L 2 o1 (NOT L) 3 QCHECK/aiger-model/examples/toggle-flip-flop.laig000644 000765 000024 00000000115 12332735360 022757 0ustar00fspedalistaff000000 000000 (model toggle-flip-flop (latch l (not l)) (output l) (output (not l))) QCHECK/aiger-model/examples/toggle-with-enable-and-reset.aag000644 000765 000024 00000000267 12332735360 024772 0ustar00fspedalistaff000000 000000 aag 7 2 1 2 4 2 4 6 8 6 7 8 4 10 10 13 15 12 2 6 14 3 7 i0 2 i1 4 l0 6 o0 6 o1 7 c model: TOGGLE-WITH-ENABLE-AND-RESET i0 ENABLE 2 i1 RESET 4 Q 6 next: NEXT-VAL 8 o0 Q 6 o1 (NOT Q) 7 QCHECK/aiger-model/examples/toggle-with-enable-and-reset.laig000644 000765 000024 00000000353 12332735360 025152 0ustar00fspedalistaff000000 000000 (model toggle-with-enable-and-reset (input enable) (input reset) (latch q next-val) (output q) (output (not q)) (and next-val reset xor) (and xor (not n1) (not n2)) (and n1 enable q) (and n2 (not enable) (not q))) QCHECK/aiger-model/examples/toggling-input.laig000644 000765 000024 00000001204 12332735360 022557 0ustar00fspedalistaff000000 000000 (model toggling-input ;; Test to make sure that the CEGAR algorithm can deal with ;; non-trivial inputs. (defblock equals (:params x y :locals and1 and2 :outputs (val eql)) (and and1 x y) (and and2 (not x) (not y)) (or-gate or1 ((x and1) (y and2)) ((val eql)))) (defblock or-gate (:params x y :locals gate :outputs (val (not gate))) (and gate (not x) (not y))) (latch l (not l)) (input i) (equals ((x i) (y l)) ((val next-l2))) (latch l2 next-l2) (latch last-eql l2) (and outval l2 last-eql) (output outval))