Skip to content
GitLab
Projects Groups Topics Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Sign in
  • E escet
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Graph
    • Compare revisions
    • Locked files
  • Issues 100
    • Issues 100
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 7
    • Merge requests 7
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Artifacts
    • Schedules
    • Test cases
  • Deployments
    • Deployments
    • Releases
  • Packages and registries
    • Packages and registries
    • Model experiments
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Eclipse ProjectsEclipse Projects
  • Eclipse ESCET (Supervisory Control Engineering Toolkit)
  • escet
  • Issues
  • #610

The CIF data-based synthesis BDD library operation ratio size should be inverted

From the code of CifDataSynthesisApp:

        double bddCacheRatio = BddOpCacheRatioOption.getCacheRatio();
	...
            bddCacheSize = (int)(bddTableSize * bddCacheRatio);
	...
            factory.setCacheRatio(bddCacheRatio);

Note how the cache ratio is used here as a fraction of the BDD node table size. It is provided to the factory via setCacheRatio. JFactory.setCacheRatio is defined as:

    public double setCacheRatio(double x) {
        return bdd_setcacheratio((int)x);
    }

This means that 1.0 becomes 1 and everything below 1.0 becomes 0.

The cache ratio is used in JFactory.bdd_operator_noderesize:

    void bdd_operator_noderesize() {
        if (cacheratio > 0) {
            int newcachesize = bddnodesize / cacheratio;

            BddCache_resize(applycache, newcachesize);
            ...
        }
    }

Here, if the cache ratio is zero, it is not resized (it stays at the initial fixed size). Interestingly, we use a *, while here a / is used. It seems we invert the meaning of the cache ratio. The factory interprets it as the number of times that the cache is smaller than the node table, while we interpret it as the fraction of the node table.

Assignee
Assign to
Time tracking

Copyright © Eclipse Foundation, Inc. All Rights Reserved.     Privacy Policy | Terms of Use | Copyright Agent